Commit 2025-01-29 06:49 e090c4ef

View on Github →

feat: the moment generating function is analytic (#20151) Define a complex-valued moment generating function and prove that it is holomorphic. As a consequence, the moment generating function is analytic on the interior of the interval on which it is finite.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Analytic/OfScalars.lean

added theorem FormalMultilinearSeries.coeff_ofScalars

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

added theorem AnalyticAt.hasFPowerSeriesAt

Modified Mathlib/Analysis/Complex/Basic.lean

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

added theorem AnalyticAt.im_ofReal

added theorem AnalyticAt.re_ofReal

added theorem AnalyticOn.im_ofReal

added theorem AnalyticOn.re_ofReal

added theorem AnalyticOnNhd.im_ofReal

added theorem AnalyticOnNhd.re_ofReal

added theorem AnalyticWithinAt.im_ofReal

added theorem AnalyticWithinAt.re_ofReal

Modified Mathlib/MeasureTheory/Integral/SetIntegral.lean

added theorem integral_complex_ofReal

Modified Mathlib/Probability/Moments/Basic.lean

added theorem ProbabilityTheory.mgf_congr_identDistrib

added theorem ProbabilityTheory.mgf_pos_iff

Created Mathlib/Probability/Moments/ComplexMGF.lean

added theorem ProbabilityTheory.abs_complexMGF_le_mgf

added theorem ProbabilityTheory.analyticAt_complexMGF

added theorem ProbabilityTheory.analyticOnNhd_complexMGF

added theorem ProbabilityTheory.analyticOn_complexMGF

added def ProbabilityTheory.complexMGF

added theorem ProbabilityTheory.complexMGF_congr_identDistrib

added theorem ProbabilityTheory.complexMGF_id_map

added theorem ProbabilityTheory.complexMGF_ofReal

added theorem ProbabilityTheory.complexMGF_undef

added theorem ProbabilityTheory.differentiableOn_complexMGF

added theorem ProbabilityTheory.eqOn_complexMGF_of_mgf'

added theorem ProbabilityTheory.eqOn_complexMGF_of_mgf

added theorem ProbabilityTheory.hasDerivAt_complexMGF

added theorem ProbabilityTheory.hasDerivAt_integral_pow_mul_exp

added theorem ProbabilityTheory.hasDerivAt_iteratedDeriv_complexMGF

added theorem ProbabilityTheory.integrableExpSet_eq_of_mgf'

added theorem ProbabilityTheory.integrableExpSet_eq_of_mgf

added theorem ProbabilityTheory.iteratedDeriv_complexMGF

added theorem ProbabilityTheory.re_complexMGF_ofReal'

added theorem ProbabilityTheory.re_complexMGF_ofReal

Modified Mathlib/Probability/Moments/IntegrableExpMul.lean

added theorem ProbabilityTheory.integrable_cexp_mul_of_re_mem_integrableExpSet

added theorem ProbabilityTheory.integrable_cexp_mul_of_re_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_abs_mul_cexp_of_re_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_abs_mul_cexp_of_re_mem_interior_integrableExpSet

added theorem ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet

Created Mathlib/Probability/Moments/MGFAnalytic.lean

added theorem ProbabilityTheory.analyticAt_mgf

added theorem ProbabilityTheory.analyticOnNhd_mgf

added theorem ProbabilityTheory.analyticOn_mgf

added theorem ProbabilityTheory.deriv_mgf

added theorem ProbabilityTheory.deriv_mgf_zero

added theorem ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real

added theorem ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf

added theorem ProbabilityTheory.hasDerivAt_mgf

added theorem ProbabilityTheory.hasFPowerSeriesAt_mgf

added theorem ProbabilityTheory.iteratedDeriv_mgf

added theorem ProbabilityTheory.iteratedDeriv_mgf_zero