Commit 2022-06-27 11:38 331df5a2

View on Github →

feat(probability/moments): moments and moment generating function of a real random variable (#14755) This PR defines moments, central moments, moment generating function and cumulant generating function.

Estimated changes

Created src/probability/moments.lean

added def probability_theory.central_moment

added theorem probability_theory.central_moment_one'

added theorem probability_theory.central_moment_one

added theorem probability_theory.central_moment_two_eq_variance

added theorem probability_theory.central_moment_zero

added def probability_theory.cgf

added theorem probability_theory.cgf_const'

added theorem probability_theory.cgf_const

added theorem probability_theory.cgf_undef

added theorem probability_theory.cgf_zero'

added theorem probability_theory.cgf_zero

added theorem probability_theory.cgf_zero_fun

added theorem probability_theory.cgf_zero_measure

added theorem probability_theory.indep_fun.cgf_add

added theorem probability_theory.indep_fun.mgf_add

added def probability_theory.mgf

added theorem probability_theory.mgf_const'

added theorem probability_theory.mgf_const

added theorem probability_theory.mgf_nonneg

added theorem probability_theory.mgf_pos'

added theorem probability_theory.mgf_pos

added theorem probability_theory.mgf_undef

added theorem probability_theory.mgf_zero'

added theorem probability_theory.mgf_zero

added theorem probability_theory.mgf_zero_fun

added theorem probability_theory.mgf_zero_measure

added def probability_theory.moment

added theorem probability_theory.moment_zero