Theorems · Theorem · probability

ProbabilityTheory.HasGaussianLaw.iIndepFun_of_covariance_strongDual

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} [Finite ι] {E : ι → Type u_3}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → MeasurableSpace (E i)]
  [∀ (i : ι), CompleteSpace (E i)] [∀ (i : ι), BorelSpace (E i)] [∀ (i : ι), SecondCountableTopology (E i)]
  [inst_5 : (i : ι) → NormedSpace ℝ (E i)] {X : (i : ι) → Ω → E i},
  ProbabilityTheory.HasGaussianLaw (fun ω i => X i ω) P →
    (∀ (i j : ι),
        i ≠ j →
          ∀ (L₁ : StrongDual ℝ (E i)) (L₂ : StrongDual ℝ (E j)),
            ProbabilityTheory.covariance (⇑L₁ ∘ X i) (⇑L₂ ∘ X j) P = 0) →
      ProbabilityTheory.iIndepFun X P

If $(X_i)_{i \in \iota}$ are jointly Gaussian and uncorrelated, then they are independent.

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Cited by

3 results in Mathlib

Foundations

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

Assumes

FiniteNormedAddCommGroupMeasurableSpaceCompleteSpaceBorelSpaceSecondCountableTopologyNormedSpace