Commit 2025-03-11 20:01 e9bb26a3

View on Github →

feat: relate tilted measure and moment generating function (#21256)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.inv_measure_univ_smul_eq_self

Modified Mathlib/Probability/Moments/Basic.lean

modified theorem ProbabilityTheory.exp_cgf

deleted theorem ProbabilityTheory.exp_cgf_of_neZero

Created Mathlib/Probability/Moments/Tilted.lean

added theorem ProbabilityTheory.integral_tilted_mul_eq_cgf

added theorem ProbabilityTheory.integral_tilted_mul_eq_mgf

added theorem ProbabilityTheory.integral_tilted_mul_self

added theorem ProbabilityTheory.memLp_tilted_mul

added theorem ProbabilityTheory.setIntegral_tilted_mul_eq_cgf'

added theorem ProbabilityTheory.setIntegral_tilted_mul_eq_cgf

added theorem ProbabilityTheory.setIntegral_tilted_mul_eq_mgf'

added theorem ProbabilityTheory.setIntegral_tilted_mul_eq_mgf

added theorem ProbabilityTheory.tilted_mul_apply_cgf'

added theorem ProbabilityTheory.tilted_mul_apply_cgf

added theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf'

added theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_cgf

added theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf'

added theorem ProbabilityTheory.tilted_mul_apply_eq_ofReal_integral_mgf

added theorem ProbabilityTheory.tilted_mul_apply_mgf'

added theorem ProbabilityTheory.tilted_mul_apply_mgf

added theorem ProbabilityTheory.variance_tilted_mul