Gaussian processes

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), Measurable (X t s)) (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), Measurable (X t s)) (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), Measurable (X t s)) (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), Measurable (X s)) (mY : ∀ (t : T), Measurable (Y t)) (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 process $(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), Measurable (X s)) (mY : ∀ (t : T), Measurable (Y t)) (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 process $(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), Measurable (X s)) (mY : ∀ (t : T), Measurable (Y t)) (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.

instance ProbabilityTheory.instBorelSpaceForallOfSubsingleton_brownianMotion {E : Type u_6} {ι : Type u_7} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] [Subsingleton ι] : BorelSpace (ι → E)

theorem ProbabilityTheory.IsGaussianProcess.indepFun'' {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : S → Ω → ℝ} {Y : T → Ω → ℝ} (h : IsGaussianProcess (Sum.elim X Y) P) (hX : ∀ (s : S), Measurable (X s)) (hY : ∀ (t : T), Measurable (Y t)) (h' : ∀ (s : S) (t : T), covariance (X s) (Y t) P = 0) : IndepFun (fun (ω : Ω) (s : S) => X s ω) (fun (ω : Ω) (t : T) => Y t ω) P

theorem ProbabilityTheory.IsGaussianProcess.iIndepFun'' {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {S : T → Type u_6} {X : (t : T) → S t → Ω → ℝ} (h : IsGaussianProcess (fun (p : (t : T) × S t) (ω : Ω) => X p.fst p.snd ω) P) (hX : ∀ (t : T) (s : S t), Measurable (X t s)) (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