Theorems · Theorem · probability

ProbabilityTheory.HasGaussianLaw.indepFun_of_covariance_eval

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

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Cited by

0 results in Mathlib

Foundations

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

Assumes

FiniteFinite