Theorems · Inductive type · probability

ProbabilityTheory.IsGaussian

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

A measure is Gaussian if its map by every continuous linear form is a real Gaussian measure.

Defined in

Mathlib.Probability.Distributions.Gaussian.Basic

Cited by

48 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommMonoidModule