Independence of Gaussian processes

This file contains properties about indepence of Gaussian processes. More precisely, we prove different versions of the following statement: if some stochastic processes are jointly Gaussian, then they are independent if their marginals are uncorrelated.

Main statements

• iIndepFun_of_covariance_eq_zero: Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and $s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $\mathrm{Cov}(X^{t_1}_{s_1}, X^{t_2}_{s_2} = 0$.

• indepFun_of_covariance_eq_zero: Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian are independent if for all $s \in S$ and $t \in T$, $\mathrm{Cov}(X_s, Y_t) = 0$.

Implementation note

To talk about the joint process of two processes X : S → Ω → E and Y : T → Ω → E, we consider the process Sum.elim X Y : S ⊕ T → Ω → E, where S ⊕ T is the disjoint union of S and T, Sum S T.

Similarly, the joint process of a family of stochastic processes X : (t : T) → (s : S t) → Ω → E is the process (p : (t : T) × S t) ↦ X p.1 p.2, where (t : T) × S t is the type of dependent pairs Sigma.

Tags

Gaussian process, independence

theorem ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_strongDual {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {S : T → Type u_4} {X : (t : T) → S t → Ω → E} [NormedSpace ℝ E] (hX : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P) (mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P) (h : ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (L₁ L₂ : StrongDual ℝ E), covariance (⇑L₁ ∘ X t₁ s₁) (⇑L₂ ∘ X t₂ s₂) P = 0) : iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P

Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and $s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.

theorem ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_inner {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {S : T → Type u_4} {X : (t : T) → S t → Ω → E} [InnerProductSpace ℝ E] (hX : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P) (mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P) (h : ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂) (x y : E), covariance (fun (ω : Ω) => inner ℝ x (X t₁ s₁ ω)) (fun (ω : Ω) => inner ℝ y (X t₂ s₂ ω)) P = 0) : iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P

Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and $s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.

theorem ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_eq_zero {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : T → Type u_4} {X : (t : T) → S t → Ω → ℝ} (hX : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P) (mX : ∀ (t : T) (s : S t), AEMeasurable (X t s) P) (h : ∀ (t₁ t₂ : T), t₁ ≠ t₂ → ∀ (s₁ : S t₁) (s₂ : S t₂), covariance (X t₁ s₁) (X t₂ s₂) P = 0) : iIndepFun (fun (t : T) (ω : Ω) (s : S t) => X t s ω) P

Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and $s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.

theorem ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_strongDual {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {S : Type u_4} {X : S → Ω → E} {Y : T → Ω → E} [NormedSpace ℝ E] (hXY : IsGaussianProcess (Sum.elim X Y) P) (mX : ∀ (s : S), AEMeasurable (X s) P) (mY : ∀ (t : T), AEMeasurable (Y t) P) (h : ∀ (s : S) (t : T) (L₁ L₂ : StrongDual ℝ E), covariance (⇑L₁ ∘ X s) (⇑L₂ ∘ Y t) P = 0) : IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P

Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.

theorem ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_inner {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [NormedAddCommGroup E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [CompleteSpace E] {S : Type u_4} {X : S → Ω → E} {Y : T → Ω → E} [InnerProductSpace ℝ E] (hXY : IsGaussianProcess (Sum.elim X Y) P) (mX : ∀ (s : S), AEMeasurable (X s) P) (mY : ∀ (t : T), AEMeasurable (Y t) P) (h : ∀ (s : S) (t : T) (x y : E), covariance (fun (ω : Ω) => inner ℝ x (X s ω)) (fun (ω : Ω) => inner ℝ y (Y t ω)) P = 0) : IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P

Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.

theorem ProbabilityTheory.IsGaussianProcess.indepFun_of_covariance_eq_zero {T : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : Type u_4} {X : S → Ω → ℝ} {Y : T → Ω → ℝ} (hXY : IsGaussianProcess (Sum.elim X Y) P) (mX : ∀ (s : S), AEMeasurable (X s) P) (mY : ∀ (t : T), AEMeasurable (Y t) P) (h : ∀ (s : S) (t : T), covariance (X s) (Y t) P = 0) : IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P

Two Gaussian processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ that are jointly Gaussian are independent if for all $s \in S$ and $t \in T$, $X_s$ and $Y_t$ are uncorrelated.