Theorems · Inductive type · probability

ProbabilityTheory.HasGaussianLaw

{Ω : Type u_1} →
  {E : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      [TopologicalSpace E] →
        [inst : AddCommMonoid E] → [Module ℝ E] → [mE : MeasurableSpace E] → (Ω → E) → MeasureTheory.Measure Ω → Prop

The predicate HasGaussianLaw X P means that under the measure P, X has a Gaussian distribution.

Defined in

Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def

Cited by

67 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommMonoidModuleMeasurableSpace