Commit 2026-03-03 17:12 92223871

View on Github →

feat: taylor expansion of the characteristic function (#36025) This is needed for CLT.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean

Renamed Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean to Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean

Created Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean

added theorem MeasureTheory.contDiff_charFun'

added theorem MeasureTheory.contDiff_charFun

added theorem MeasureTheory.continuous_charFun

added theorem MeasureTheory.iteratedDeriv_charFun

added theorem MeasureTheory.iteratedDeriv_charFun_zero

added theorem MeasureTheory.iteratedFDeriv_charFun

added theorem MeasureTheory.taylorWithinEval_charFun_two_zero'

added theorem MeasureTheory.taylorWithinEval_charFun_two_zero

added theorem MeasureTheory.taylorWithinEval_charFun_zero

Modified Mathlib/MeasureTheory/Measure/IntegralCharFun.lean

Modified Mathlib/Probability/Independence/CharacteristicFunction.lean

Modified Mathlib/Probability/Moments/ComplexMGF.lean

modified def ProbabilityTheory.complexMGF