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 variableXhas a Gaussian distribution under the measureP.
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 Ω)
:
The predicate HasGaussianLaw X P means that under the measure P,
X has a Gaussian distribution.
- isGaussian_map : IsGaussian (MeasureTheory.Measure.map X P)