Commit 2025-01-02 20:19 670870be

View on Github →

feat(Probability/Distributions/Gaussian): the mgf of a gaussian (#19896) Compute the mgf of a gaussian.

Estimated changes

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem AEMeasurable.of_map_ne_zero

Modified Mathlib/Probability/Distributions/Gaussian.lean

added theorem ProbabilityTheory.cgf_gaussianReal

added theorem ProbabilityTheory.mgf_gaussianReal

Modified Mathlib/Probability/Moments.lean

added theorem ProbabilityTheory.mgf_add_const

added theorem ProbabilityTheory.mgf_const_add

added theorem ProbabilityTheory.mgf_dirac

added theorem ProbabilityTheory.mgf_id_map