Theorem MeasureTheory.taylorWithinEval_charFun_two_zero'

Modification history

2026-03-03 17:12
Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean
feat: taylor expansion of the characteristic function (#36025) …
Added MeasureTheory.taylorWithinEval_charFun_two_zero'View on Github →