Independence of Gaussian random variables #
In this file we prove some results linking Gaussian random variables and independence. It is
a well known fact that if (X, Y) is Gaussian, then X and Y are independent if their covariance
is zero. We prove many versions of this theorem in different settings: in Banach spaces,
Hilbert spaces, and for families of real random variables.
We also prove that independent Gaussian random variables are jointly Gaussian.
Main statements #
iIndepFun.hasGaussianLaw: Independent Gaussian random variables are jointly Gaussian, indexed version.IndepFun.hasGaussianLaw: Independent Gaussian random variables are jointly Gaussian, product version.HasGaussianLaw.iIndepFun_of_covariance_eq_zero: If $(X_i)_{i \in \iota}$ are jointly Gaussian, then they are independent if for all $i \ne j$, \mathrm{Cov}(X_i, X_j) = 0$.HasGaussianLaw.indepFun_of_covariance_eq_zero: If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if $\mathrm{Cov}(X, Y) = 0$.
Tags #
Gaussian random variable
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_2}
[Finite ι]
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
{X : (i : ι) → Ω → E i}
(hX1 : ∀ (i : ι), HasGaussianLaw (X i) P)
(hX2 : iIndepFun X P)
:
HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P
Independent Gaussian random variables are jointly Gaussian.
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_2}
[Finite ι]
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
[(i : ι) → NormedSpace ℝ (E i)]
{X : (i : ι) → Ω → E i}
(hX : HasGaussianLaw (fun (ω : Ω) (i : ι) => X i ω) P)
(h :
∀ (i j : ι), i ≠ j → ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)), covariance (⇑L₁ ∘ X i) (⇑L₂ ∘ X j) P = 0)
:
iIndepFun X P
If $(X_i)_{i \in \iota}$ are jointly Gaussian and uncorrelated, then they are independent.
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_inner
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_2}
[Finite ι]
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → MeasurableSpace (E i)]
[∀ (i : ι), CompleteSpace (E i)]
[∀ (i : ι), BorelSpace (E i)]
[∀ (i : ι), SecondCountableTopology (E i)]
[(i : ι) → InnerProductSpace ℝ (E i)]
{X : (i : ι) → Ω → E i}
(hX : HasGaussianLaw (fun (ω : Ω) (i : ι) => X i ω) P)
(h :
∀ (i j : ι),
i ≠ j →
∀ (x : E i) (y : E j), covariance (fun (ω : Ω) => inner ℝ x (X i ω)) (fun (ω : Ω) => inner ℝ y (X j ω)) P = 0)
:
iIndepFun X P
If $(X_i)_{i \in \iota}$ are jointly Gaussian and uncorrelated, then they are independent.
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eval
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_2}
[Finite ι]
{κ : ι → Type u_4}
[∀ (i : ι), Finite (κ i)]
{X : (i : ι) → κ i → Ω → ℝ}
(hX : HasGaussianLaw (fun (ω : Ω) (i : ι) (j : κ i) => X i j ω) P)
(h : ∀ (i j : ι), i ≠ j → ∀ (k : κ i) (l : κ j), covariance (X i k) (X j l) P = 0)
:
iIndepFun (fun (i : ι) (ω : Ω) (j : κ i) => X i j ω) P
If $((X_{i,j})_{j \in \kappa_i})_{i \in \iota}$ are jointly Gaussian, then they are independent if for all $i_1 \ne i_2 \in \iota$ and for all $j_1 \in \kappa_{i_1}, j_2 \in \kappa_{i_2}$, $\mathrm{Cov}(X_{i_1, j_1}, X_{i_2, j_2}) = 0$.
theorem
ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_2}
[Finite ι]
{X : ι → Ω → ℝ}
(hX : HasGaussianLaw (fun (ω : Ω) (x : ι) => X x ω) P)
(h : ∀ (i j : ι), i ≠ j → covariance (X i) (X j) P = 0)
:
iIndepFun X P
If $(X_i)_{i \in \iota}$ are jointly Gaussian, then they are independent if for all $i \ne j$, \mathrm{Cov}(X_i, X_j) = 0$.
theorem
ProbabilityTheory.IndepFun.hasGaussianLaw
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[MeasurableSpace E]
[CompleteSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[NormedAddCommGroup F]
[MeasurableSpace F]
[CompleteSpace F]
[BorelSpace F]
[SecondCountableTopology F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
{X : Ω → E}
{Y : Ω → F}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(hXY : IndepFun X Y P)
:
HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P
Independent Gaussian random variables are jointly Gaussian.
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_strongDual
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[MeasurableSpace E]
[CompleteSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[NormedAddCommGroup F]
[MeasurableSpace F]
[CompleteSpace F]
[BorelSpace F]
[SecondCountableTopology F]
[NormedSpace ℝ E]
[NormedSpace ℝ F]
{X : Ω → E}
{Y : Ω → F}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(h : ∀ (L₁ : StrongDual ℝ E) (L₂ : StrongDual ℝ F), covariance (⇑L₁ ∘ X) (⇑L₂ ∘ Y) P = 0)
:
IndepFun X Y P
If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if they are uncorrelated.
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_inner
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
{F : Type u_3}
[NormedAddCommGroup E]
[MeasurableSpace E]
[CompleteSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[NormedAddCommGroup F]
[MeasurableSpace F]
[CompleteSpace F]
[BorelSpace F]
[SecondCountableTopology F]
[InnerProductSpace ℝ E]
[InnerProductSpace ℝ F]
{X : Ω → E}
{Y : Ω → F}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(h : ∀ (x : E) (y : F), covariance (fun (ω : Ω) => inner ℝ x (X ω)) (fun (ω : Ω) => inner ℝ y (Y ω)) P = 0)
:
IndepFun X Y P
If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if they are uncorrelated.
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eval
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{ι : Type u_4}
{κ : Type u_5}
[Finite ι]
[Finite κ]
{X : ι → Ω → ℝ}
{Y : κ → Ω → ℝ}
(hXY : HasGaussianLaw (fun (ω : Ω) => (fun (i : ι) => X i ω, fun (j : κ) => Y j ω)) P)
(h : ∀ (i : ι) (j : κ), covariance (X i) (Y j) P = 0)
:
IndepFun (fun (ω : Ω) (i : ι) => X i ω) (fun (ω : Ω) (j : κ) => Y j ω) P
If $((X_i)_{i \in \iota}, (Y_j)_{j \in \kappa})$ is Gaussian, then $(X_i)_{i \in \iota}$ and $(Y_j)_{j \in \kappa}$ are independent if for all $i \in \iota, j \in \kappa$, $\mathrm{Cov}(X_i, Y_j) = 0$.
theorem
ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eq_zero
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{X Y : Ω → ℝ}
(hXY : HasGaussianLaw (fun (ω : Ω) => (X ω, Y ω)) P)
(h : covariance X Y P = 0)
:
IndepFun X Y P
If $(X, Y)$ is Gaussian, then $X$ and $Y$ are independent if $\mathrm{Cov}(X, Y) = 0$.
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_sum
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{ι : Type u_3}
[Fintype ι]
{X : ι → Ω → E}
(hX1 : ∀ (i : ι), HasGaussianLaw (X i) P)
(hX2 : iIndepFun X P)
:
HasGaussianLaw (∑ i : ι, X i) P
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_sum
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{ι : Type u_3}
[Fintype ι]
{X : ι → Ω → E}
(hX1 : ∀ (i : ι), HasGaussianLaw (X i) P)
(hX2 : iIndepFun X P)
:
HasGaussianLaw (fun (ω : Ω) => ∑ i : ι, X i ω) P
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_add
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X Y P)
:
HasGaussianLaw (X + Y) P
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_add
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X Y P)
:
HasGaussianLaw (fun (ω : Ω) => X ω + Y ω) P
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_sub
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X Y P)
:
HasGaussianLaw (X - Y) P
theorem
ProbabilityTheory.iIndepFun.hasGaussianLaw_fun_sub
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
[CompleteSpace E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X Y P)
:
HasGaussianLaw (fun (ω : Ω) => X ω - Y ω) P
theorem
ProbabilityTheory.IndepFun.hasGaussianLaw_sub_of_sub
{Ω : Type u_1}
{mΩ : MeasurableSpace Ω}
{P : MeasureTheory.Measure Ω}
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[MeasurableSpace E]
[BorelSpace E]
[SecondCountableTopology E]
{X Y : Ω → E}
(hX : HasGaussianLaw X P)
(hY : HasGaussianLaw Y P)
(h : IndepFun X (Y - X) P)
:
HasGaussianLaw (Y - X) P
If X and Y are two Gaussian random variables such that X and Y - X are independent,
then Y - X is Gaussian.
This lemma is useful to prove that a process with independent increments and whose marginals are Gaussian has Gaussian increments.