Commit 2025-02-05 11:40 ad7930c3

View on Github →

feat(Probability): first two derivatives of cgf (#21223)

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean

added theorem AnalyticAt.log

added theorem AnalyticOn.log

added theorem AnalyticOnNhd.log

added theorem AnalyticWithinAt.log

added theorem analyticAt_log

added theorem analyticOnNhd_log

added theorem analyticOn_log

Modified Mathlib/Probability/Moments/Basic.lean

modified theorem ProbabilityTheory.cgf_zero_measure

modified theorem ProbabilityTheory.mgf_zero_measure

Modified Mathlib/Probability/Moments/MGFAnalytic.lean

added theorem ProbabilityTheory.analyticAt_cgf

added theorem ProbabilityTheory.analyticAt_iteratedDeriv_mgf

added theorem ProbabilityTheory.analyticOnNhd_cgf

added theorem ProbabilityTheory.analyticOnNhd_iteratedDeriv_mgf

added theorem ProbabilityTheory.analyticOn_cgf

added theorem ProbabilityTheory.analyticOn_iteratedDeriv_mgf

added theorem ProbabilityTheory.deriv_cgf

added theorem ProbabilityTheory.deriv_cgf_zero

added theorem ProbabilityTheory.differentiableAt_iteratedDeriv_mgf

added theorem ProbabilityTheory.differentiableAt_mgf

added theorem ProbabilityTheory.iteratedDeriv_two_cgf

added theorem ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral