Theorem MeasureTheory.contDiff_charFun

Modification history

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