Commit 2025-04-23 09:00 942869ba

View on Github →

feat(Probability): characteristic function of a Gaussian distribution (#24289) Characteristic function and complex moment generating function of Gaussian distributions.

Estimated changes

Modified Mathlib/Probability/Distributions/Gaussian.lean

added theorem ProbabilityTheory.charFun_gaussianReal

added theorem ProbabilityTheory.complexMGF_gaussianReal

added theorem ProbabilityTheory.complexMGF_id_gaussianReal

added theorem ProbabilityTheory.gaussianPDF_lt_top

added theorem ProbabilityTheory.gaussianPDF_ne_top

modified theorem ProbabilityTheory.gaussianPDF_zero_var

added theorem ProbabilityTheory.integral_gaussianReal_eq_integral_smul

added theorem ProbabilityTheory.toReal_gaussianPDF

Modified Mathlib/Probability/Moments/ComplexMGF.lean

added theorem ProbabilityTheory.complexMGF_id_mul_I

added theorem ProbabilityTheory.complexMGF_mul_I