Theorems · Theorem · probability

ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_eq_zero

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {X : ι → Ω → ℝ},
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P →
    (∀ (i j : ι), i ≠ j → ProbabilityTheory.covariance (X i) (X j) P = 0) → ProbabilityTheory.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$.

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Cited by

1 results in Mathlib

Foundations

Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Finite