Skip to content

Commit df8d6a9

Browse files
EtienneC30EtienneC30
committed
feat: links between characteristic function and independence (leanprover-community#26269)
Prove several results of the form: random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. More specifically, prove this in Hilbert spaces for two variables and a finite family of variables. Same in Banach spaces, with an arbitrary Lp norm. Co-authored-by: Etienne Marion <baguettes_casino0c@icloud.com>
1 parent 9aeba39 commit df8d6a9

2 files changed

Lines changed: 130 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5271,6 +5271,7 @@ import Mathlib.Probability.Distributions.Uniform
52715271
import Mathlib.Probability.HasLaw
52725272
import Mathlib.Probability.IdentDistrib
52735273
import Mathlib.Probability.Independence.Basic
5274+
import Mathlib.Probability.Independence.CharacteristicFunction
52745275
import Mathlib.Probability.Independence.Conditional
52755276
import Mathlib.Probability.Independence.InfinitePi
52765277
import Mathlib.Probability.Independence.Integrable

‎Mathlib/Probability/Independence/CharacteristicFunction.lean‎

Lines changed: 129 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,129 @@
1+
/-
2+
Copyright (c) 2025 Etienne Marion. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Etienne Marion
5+
-/
6+
import Mathlib.MeasureTheory.Measure.CharacteristicFunction
7+
import Mathlib.Probability.Independence.Basic
8+
9+
/-!
10+
# Links between independence and characteristic function
11+
12+
Two random variables are independent if and only if their joint characteristic function is equal
13+
to the product of the characteristic functions. More specifically, prove this in Hilbert spaces for
14+
two variables and a finite family of variables. We prove the analoguous statemens in Banach spaces,
15+
with an arbitrary Lp norm, for the dual characteristic function.
16+
-/
17+
18+
namespace ProbabilityTheory
19+
20+
open MeasureTheory WithLp
21+
open scoped ENNReal
22+
23+
variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {P : Measure Ω}
24+
(p : ℝ≥0∞) [Fact (1 ≤ p)]
25+
26+
section IndepFun
27+
28+
variable [IsFiniteMeasure P] {E F : Type*}
29+
{mE : MeasurableSpace E} [NormedAddCommGroup E] [CompleteSpace E]
30+
[BorelSpace E] [SecondCountableTopology E]
31+
{mF : MeasurableSpace F} [NormedAddCommGroup F] [CompleteSpace F]
32+
[BorelSpace F] [SecondCountableTopology F]
33+
{X : Ω → E} {Y : Ω → F}
34+
35+
section InnerProductSpace
36+
37+
variable [InnerProductSpace ℝ E] [InnerProductSpace ℝ F]
38+
39+
/-- Two random variables are independent if and only if their joint characteristic function is equal
40+
to the product of the characteristic functions. This is the version for Hilbert spaces, see
41+
`indepFun_iff_charFunDual_prod` for the Banach space version. -/
42+
lemma indepFun_iff_charFun_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
43+
IndepFun X Y P ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X ω, Y ω))) t =
44+
charFun (P.map X) t.ofLp.1 * charFun (P.map Y) t.ofLp.2 := by
45+
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFun_eq_prod_iff,
46+
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
47+
48+
end InnerProductSpace
49+
50+
section NormedSpace
51+
52+
variable [NormedSpace ℝ E] [NormedSpace ℝ F]
53+
54+
/-- Two random variables are independent if and only if their joint characteristic function is equal
55+
to the product of the characteristic functions. This is the version for Banach spaces, see
56+
`indepFun_iff_charFun_prod` for the Hilbert space version. -/
57+
lemma indepFun_iff_charFunDual_prod (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
58+
IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X ω, Y ω))) L =
59+
charFunDual (P.map X) (L.comp (.inl ℝ E F)) *
60+
charFunDual (P.map Y) (L.comp (.inr ℝ E F)) := by
61+
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff]
62+
63+
/-- Two random variables are independent if and only if their joint characteristic function is equal
64+
to the product of the characteristic functions. This is `indepFun_iff_charFunDual_prod` for
65+
`WithLp`. See `indepFun_iff_charFun_prod` for the Hilbert space version. -/
66+
lemma indepFun_iff_charFunDual_prod' (hX : AEMeasurable X P) (hY : AEMeasurable Y P) :
67+
IndepFun X Y P ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X ω, Y ω))) L =
68+
charFunDual (P.map X) (L.comp
69+
((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp
70+
(.inl ℝ E F))) *
71+
charFunDual (P.map Y) (L.comp
72+
((prodContinuousLinearEquiv p ℝ E F).symm.toContinuousLinearMap.comp
73+
(.inr ℝ E F))) := by
74+
rw [indepFun_iff_map_prod_eq_prod_map_map hX hY, ← charFunDual_eq_prod_iff' p,
75+
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
76+
77+
end NormedSpace
78+
79+
end IndepFun
80+
81+
section iIndepFun
82+
83+
variable [IsProbabilityMeasure P] {ι : Type*} [Fintype ι] {E : ι → Type*}
84+
{mE : ∀ i, MeasurableSpace (E i)} [∀ i, NormedAddCommGroup (E i)] [∀ i, CompleteSpace (E i)]
85+
[∀ i, BorelSpace (E i)] [∀ i, SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i}
86+
87+
section InnerProductSpace
88+
89+
variable [∀ i, InnerProductSpace ℝ (E i)]
90+
91+
/-- A finite number of random variables are independent if and only if their joint characteristic
92+
function is equal to the product of the characteristic functions. This is the version for Hilbert
93+
spaces, see `iIndepFun_iff_charFunDual_pi` for the Hilbert space version. -/
94+
lemma iIndepFun_iff_charFun_pi (hX : ∀ i, AEMeasurable (X i) P) :
95+
iIndepFun X P ↔ ∀ t, charFun (P.map (fun ω ↦ toLp 2 (X · ω))) t =
96+
∏ i, charFun (P.map (X i)) (t i) := by
97+
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFun_eq_pi_iff,
98+
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
99+
100+
end InnerProductSpace
101+
102+
section NormedSpace
103+
104+
variable [∀ i, NormedSpace ℝ (E i)] [DecidableEq ι]
105+
106+
/-- A finite number of random variables are independent if and only if their joint characteristic
107+
function is equal to the product of the characteristic functions. This is the version for Banach
108+
spaces, see `iIndepFun_iff_charFun_pi` for the Hilbert space version. -/
109+
lemma iIndepFun_iff_charFunDual_pi (hX : ∀ i, AEMeasurable (X i) P) :
110+
iIndepFun X P ↔ ∀ L, charFunDual (P.map (fun ω ↦ (X · ω))) L =
111+
∏ i, charFunDual (P.map (X i)) (L.comp (.single ℝ E i)) := by
112+
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff]
113+
114+
/-- A finite number of random variables are independent if and only if their joint characteristic
115+
function is equal to the product of the characteristic functions.
116+
This is `iIndepFun_iff_charFunDual_pi` for `WithLp`. See `iIndepFun_iff_charFun_pi` for the
117+
Hilbert space version. -/
118+
lemma iIndepFun_iff_charFunDual_pi' (hX : ∀ i, AEMeasurable (X i) P) :
119+
iIndepFun X P ↔ ∀ L, charFunDual (P.map (fun ω ↦ toLp p (X · ω))) L =
120+
∏ i, charFunDual (P.map (X i)) (L.comp
121+
((PiLp.continuousLinearEquiv p ℝ E).symm.toContinuousLinearMap.comp (.single ℝ E i))) := by
122+
rw [iIndepFun_iff_map_fun_eq_pi_map hX, ← charFunDual_eq_pi_iff' p,
123+
AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop), Function.comp_def]
124+
125+
end NormedSpace
126+
127+
end iIndepFun
128+
129+
end ProbabilityTheory

0 commit comments

Comments
 (0)