Commit 2026-01-26 14:59 ae6ea95b

View on Github →

feat: add a predicate HasGaussianLaw (#32144) Define a predicate HasGaussianLaw X P, which states that under the measure P, the random variable X has a Gaussian distribution, i.e. IsGaussian (P.map X).

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Basic.lean

added theorem ProbabilityTheory.HasGaussianLaw.add

added theorem ProbabilityTheory.HasGaussianLaw.aemeasurable

added theorem ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq

added theorem ProbabilityTheory.HasGaussianLaw.charFunDual_map_eq_fun

added theorem ProbabilityTheory.HasGaussianLaw.charFun_map_eq

added theorem ProbabilityTheory.HasGaussianLaw.congr

added theorem ProbabilityTheory.HasGaussianLaw.eval

added theorem ProbabilityTheory.HasGaussianLaw.fst

added theorem ProbabilityTheory.HasGaussianLaw.fun_add

added theorem ProbabilityTheory.HasGaussianLaw.fun_neg

added theorem ProbabilityTheory.HasGaussianLaw.fun_smul

added theorem ProbabilityTheory.HasGaussianLaw.fun_sub

added theorem ProbabilityTheory.HasGaussianLaw.fun_sum

added theorem ProbabilityTheory.HasGaussianLaw.integrable

added theorem ProbabilityTheory.HasGaussianLaw.isProbabilityMeasure

added theorem ProbabilityTheory.HasGaussianLaw.map

added theorem ProbabilityTheory.HasGaussianLaw.map_equiv

added theorem ProbabilityTheory.HasGaussianLaw.map_equiv_fun

added theorem ProbabilityTheory.HasGaussianLaw.map_fun

added theorem ProbabilityTheory.HasGaussianLaw.map_of_measurable

added theorem ProbabilityTheory.HasGaussianLaw.memLp

added theorem ProbabilityTheory.HasGaussianLaw.memLp_two

added theorem ProbabilityTheory.HasGaussianLaw.neg

added theorem ProbabilityTheory.HasGaussianLaw.prodMk

added theorem ProbabilityTheory.HasGaussianLaw.smul

added theorem ProbabilityTheory.HasGaussianLaw.snd

added theorem ProbabilityTheory.HasGaussianLaw.sub

added theorem ProbabilityTheory.HasGaussianLaw.sum

added theorem ProbabilityTheory.HasGaussianLaw.toLp_pi

added theorem ProbabilityTheory.HasGaussianLaw.toLp_prodMk

added theorem ProbabilityTheory.HasLaw.hasGaussianLaw

added theorem ProbabilityTheory.IsGaussian.hasGaussianLaw

added theorem ProbabilityTheory.IsGaussian.hasGaussianLaw_id

added theorem ProbabilityTheory.hasGaussianLaw_iff_charFunDual_map_eq

added theorem ProbabilityTheory.hasGaussianLaw_iff_charFun_map_eq

Created Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Def.lean