Theorems · Theorem · probability

ProbabilityTheory.iIndepFun.hasGaussianLaw

∀ {Ω : 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},
  (∀ (i : ι), ProbabilityTheory.HasGaussianLaw (X i) P) →
    ProbabilityTheory.iIndepFun X P → ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P

Independent Gaussian random variables are jointly Gaussian.

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Cited by

3 results in Mathlib

Foundations

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

Assumes

FiniteNormedAddCommGroupMeasurableSpaceCompleteSpaceBorelSpaceSecondCountableTopologyNormedSpace