Gaussian random variables

In this file we define a predicate HasGaussianLaw X P, which states that under the probability measure P, the random variable X has a Gaussian distribution, i.e. IsGaussian (P.map X).

Main definition

• HasGaussianLaw X P: The random variable X has a Gaussian distribution under the measure P.

Tags

Gaussian random variable

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

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

• aemeasurable : AEMeasurable X P
• isGaussian_map : IsGaussian (MeasureTheory.Measure.map X P)