Gaussian processes #
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