Commit 2025-01-08 08:24 7a48271e

View on Github →

feat: misc. lemmas about moments, tilted measures (#20150)

Estimated changes

Modified Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean

modified theorem Real.aemeasurable_of_aemeasurable_exp

added theorem Real.aemeasurable_of_aemeasurable_exp_mul

modified theorem Real.measurable_of_measurable_exp

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

Modified Mathlib/MeasureTheory/Order/Group/Lattice.lean

Modified Mathlib/Probability/Moments.lean

added theorem ProbabilityTheory.centralMoment_zero_measure

added theorem ProbabilityTheory.exp_cgf

added theorem ProbabilityTheory.exp_cgf_of_neZero

added theorem ProbabilityTheory.moment_zero_measure