Links between independence and characteristic function

Two 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. We prove the analoguous statemens in Banach spaces, with an arbitrary Lp norm, for the dual characteristic function.

theorem ProbabilityTheory.indepFun_iff_charFun_prod {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2} {F : Type u_3} {mE : MeasurableSpace E} [NormedAddCommGroup E] [CompleteSpace E] [BorelSpace E] [SecondCountableTopology E] {mF : MeasurableSpace F} [NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F] {X : Ω → E} {Y : Ω → F} [InnerProductSpace ℝ E] [InnerProductSpace ℝ F] (hX : AEMeasurable X P) (hY : AEMeasurable Y P) : IndepFun X Y P ↔ ∀ (t : WithLp 2 (E × F)), MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 (X ω, Y ω)) P) t = MeasureTheory.charFun (MeasureTheory.Measure.map X P) t.ofLp.1 * MeasureTheory.charFun (MeasureTheory.Measure.map Y P) t.ofLp.2

Two random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is the version for Hilbert spaces, see indepFun_iff_charFunDual_prod for the Banach space version.

theorem ProbabilityTheory.indepFun_iff_charFunDual_prod {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {E : Type u_2} {F : Type u_3} {mE : MeasurableSpace E} [NormedAddCommGroup E] [CompleteSpace E] [BorelSpace E] [SecondCountableTopology E] {mF : MeasurableSpace F} [NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F] {X : Ω → E} {Y : Ω → F} [NormedSpace ℝ E] [NormedSpace ℝ F] (hX : AEMeasurable X P) (hY : AEMeasurable Y P) : IndepFun X Y P ↔ ∀ (L : StrongDual ℝ (E × F)), MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun (ω : Ω) => (X ω, Y ω)) P) L = MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) (ContinuousLinearMap.comp L (ContinuousLinearMap.inl ℝ E F)) * MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P) (ContinuousLinearMap.comp L (ContinuousLinearMap.inr ℝ E F))

Two random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is the version for Banach spaces, see indepFun_iff_charFun_prod for the Hilbert space version.

theorem ProbabilityTheory.indepFun_iff_charFunDual_prod' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (p : ENNReal) [Fact (1 ≤ p)] [MeasureTheory.IsFiniteMeasure P] {E : Type u_2} {F : Type u_3} {mE : MeasurableSpace E} [NormedAddCommGroup E] [CompleteSpace E] [BorelSpace E] [SecondCountableTopology E] {mF : MeasurableSpace F} [NormedAddCommGroup F] [CompleteSpace F] [BorelSpace F] [SecondCountableTopology F] {X : Ω → E} {Y : Ω → F} [NormedSpace ℝ E] [NormedSpace ℝ F] (hX : AEMeasurable X P) (hY : AEMeasurable Y P) : IndepFun X Y P ↔ ∀ (L : StrongDual ℝ (WithLp p (E × F))), MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp p (X ω, Y ω)) P) L = MeasureTheory.charFunDual (MeasureTheory.Measure.map X P) (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inl ℝ E F))) * MeasureTheory.charFunDual (MeasureTheory.Measure.map Y P) (ContinuousLinearMap.comp L ((↑(WithLp.prodContinuousLinearEquiv p ℝ E F).symm).comp (ContinuousLinearMap.inr ℝ E F)))

Two random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is indepFun_iff_charFunDual_prod for WithLp. See indepFun_iff_charFun_prod for the Hilbert space version.

theorem ProbabilityTheory.iIndepFun_iff_charFun_pi {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)} [(i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [(i : ι) → InnerProductSpace ℝ (E i)] (hX : ∀ (i : ι), AEMeasurable (X i) P) : iIndepFun X P ↔ ∀ (t : WithLp 2 ((x : ι) → E x)), MeasureTheory.charFun (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp 2 fun (x : ι) => X x ω) P) t = ∏ i : ι, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P) (t i)

A finite number of random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is the version for Hilbert spaces, see iIndepFun_iff_charFunDual_pi for the Hilbert space version.

theorem ProbabilityTheory.iIndepFun_iff_charFunDual_pi {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)} [(i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [(i : ι) → NormedSpace ℝ (E i)] [DecidableEq ι] (hX : ∀ (i : ι), AEMeasurable (X i) P) : iIndepFun X P ↔ ∀ (L : StrongDual ℝ ((x : ι) → E x)), MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun (ω : Ω) (x : ι) => X x ω) P) L = ∏ i : ι, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P) (ContinuousLinearMap.comp L (ContinuousLinearMap.single ℝ E i))

A finite number of random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is the version for Banach spaces, see iIndepFun_iff_charFun_pi for the Hilbert space version.

theorem ProbabilityTheory.iIndepFun_iff_charFunDual_pi' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (p : ENNReal) [Fact (1 ≤ p)] [MeasureTheory.IsProbabilityMeasure P] {ι : Type u_2} [Fintype ι] {E : ι → Type u_3} {mE : (i : ι) → MeasurableSpace (E i)} [(i : ι) → NormedAddCommGroup (E i)] [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)] {X : (i : ι) → Ω → E i} [(i : ι) → NormedSpace ℝ (E i)] [DecidableEq ι] (hX : ∀ (i : ι), AEMeasurable (X i) P) : iIndepFun X P ↔ ∀ (L : StrongDual ℝ (WithLp p ((x : ι) → E x))), MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun (ω : Ω) => WithLp.toLp p fun (x : ι) => X x ω) P) L = ∏ i : ι, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P) (ContinuousLinearMap.comp L ((↑(PiLp.continuousLinearEquiv p ℝ E).symm).comp (ContinuousLinearMap.single ℝ E i)))

A finite number of random variables are independent if and only if their joint characteristic function is equal to the product of the characteristic functions. This is iIndepFun_iff_charFunDual_pi for WithLp. See iIndepFun_iff_charFun_pi for the Hilbert space version.