Commit 2023-06-21 09:25 9da26a02

View on Github →

feat: port Probability.Moments (#5338) This PR completes the port of the entire Probability folder to mathlib4.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Probability/Moments.lean

added theorem ProbabilityTheory.IndepFun.cgf_add

added theorem ProbabilityTheory.IndepFun.exp_mul

added theorem ProbabilityTheory.IndepFun.integrable_exp_mul_add

added theorem ProbabilityTheory.IndepFun.mgf_add'

added theorem ProbabilityTheory.IndepFun.mgf_add

added theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_add

added theorem ProbabilityTheory.aestronglyMeasurable_exp_mul_sum

added def ProbabilityTheory.centralMoment

added theorem ProbabilityTheory.centralMoment_one'

added theorem ProbabilityTheory.centralMoment_one

added theorem ProbabilityTheory.centralMoment_two_eq_variance

added theorem ProbabilityTheory.centralMoment_zero

added def ProbabilityTheory.cgf

added theorem ProbabilityTheory.cgf_const'

added theorem ProbabilityTheory.cgf_const

added theorem ProbabilityTheory.cgf_neg

added theorem ProbabilityTheory.cgf_undef

added theorem ProbabilityTheory.cgf_zero'

added theorem ProbabilityTheory.cgf_zero

added theorem ProbabilityTheory.cgf_zero_fun

added theorem ProbabilityTheory.cgf_zero_measure

added theorem ProbabilityTheory.iIndepFun.cgf_sum

added theorem ProbabilityTheory.iIndepFun.integrable_exp_mul_sum

added theorem ProbabilityTheory.iIndepFun.mgf_sum

added theorem ProbabilityTheory.measure_ge_le_exp_cgf

added theorem ProbabilityTheory.measure_ge_le_exp_mul_mgf

added theorem ProbabilityTheory.measure_le_le_exp_cgf

added theorem ProbabilityTheory.measure_le_le_exp_mul_mgf

added def ProbabilityTheory.mgf

added theorem ProbabilityTheory.mgf_const'

added theorem ProbabilityTheory.mgf_const

added theorem ProbabilityTheory.mgf_neg

added theorem ProbabilityTheory.mgf_nonneg

added theorem ProbabilityTheory.mgf_pos'

added theorem ProbabilityTheory.mgf_pos

added theorem ProbabilityTheory.mgf_undef

added theorem ProbabilityTheory.mgf_zero'

added theorem ProbabilityTheory.mgf_zero

added theorem ProbabilityTheory.mgf_zero_fun

added theorem ProbabilityTheory.mgf_zero_measure

added def ProbabilityTheory.moment

added theorem ProbabilityTheory.moment_zero