Theorems · Theorem · probability

ProbabilityTheory.HasGaussianLaw.prodMk

∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {E : ι → Type u_5}
  [inst : (i : ι) → NormedAddCommGroup (E i)] [inst_1 : (i : ι) → NormedSpace ℝ (E i)]
  [inst_2 : (i : ι) → MeasurableSpace (E i)] [∀ (i : ι), BorelSpace (E i)] {X : (i : ι) → Ω → E i}
  [∀ (i : ι), SecondCountableTopology (E i)] [Finite ι],
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P →
    ∀ (i j : ι), ProbabilityTheory.HasGaussianLaw (fun ω => (X i ω, X j ω)) P

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceSecondCountableTopologyFinite