Theorems · Theorem · probability

ProbabilityTheory.HasGaussianLaw.eval

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

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpace