Commit 2025-04-14 06:29 190e6855

View on Github →

feat(MeasureTheory): characteristic function in an inner product space (#23973) Add a definition of a characteristic function, which is equal to the integral of BoundedContinuousFunction.char for the inner product bilinear map and the additive character e = Real.probChar.

Estimated changes

Modified Mathlib/Analysis/Complex/Circle.lean

Modified Mathlib/Analysis/Fourier/FourierTransform.lean

added theorem VectorFourier.fourierIntegral_probChar

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

added def BoundedContinuousFunction.innerProbChar

added theorem BoundedContinuousFunction.innerProbChar_apply

added theorem BoundedContinuousFunction.innerProbChar_zero

added theorem MeasureTheory.Measure.ext_of_charFun

added theorem MeasureTheory.charFun_apply

added theorem MeasureTheory.charFun_apply_real

added theorem MeasureTheory.charFun_eq_fourierIntegral'

added theorem MeasureTheory.charFun_eq_fourierIntegral

added theorem MeasureTheory.charFun_eq_integral_innerProbChar

added theorem MeasureTheory.charFun_eq_integral_probChar

added theorem MeasureTheory.charFun_map_mul

added theorem MeasureTheory.charFun_map_smul

added theorem MeasureTheory.charFun_neg

added theorem MeasureTheory.charFun_zero

added theorem MeasureTheory.charFun_zero_measure

added theorem MeasureTheory.intervalIntegrable_charFun

added theorem MeasureTheory.measurable_charFun

added theorem MeasureTheory.norm_charFun_le

added theorem MeasureTheory.norm_charFun_le_one

added theorem MeasureTheory.norm_one_sub_charFun_le_two

added theorem MeasureTheory.stronglyMeasurable_charFun