Commit 2025-05-15 20:48 826c8f09

View on Github →

feat(MeasureTheory): characteristic function in a Banach space (#24836) Define charFunDual μ L, the characteristic function of a measure μ at L : Dual ℝ E in a normed space E. This is the integral ∫ v, exp (L v * I) ∂μ.

Estimated changes

Modified Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

added theorem IsBoundedBilinearMap.symm

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

added def BoundedContinuousFunction.probCharDual

added theorem BoundedContinuousFunction.probCharDual_apply

added theorem BoundedContinuousFunction.probCharDual_zero

modified theorem MeasureTheory.Measure.ext_of_charFun

added theorem MeasureTheory.Measure.ext_of_charFunDual

added def MeasureTheory.charFunDual

added theorem MeasureTheory.charFunDual_apply

added theorem MeasureTheory.charFunDual_dirac

added theorem MeasureTheory.charFunDual_eq_charFun_map_one

added theorem MeasureTheory.charFunDual_map

added theorem MeasureTheory.charFunDual_prod

added theorem MeasureTheory.charFun_eq_charFunDual_toDualMap

added theorem MeasureTheory.charFun_map_eq_charFunDual_smul

Modified Mathlib/Topology/Algebra/Module/LinearMapPiProd.lean

added theorem ContinuousLinearMap.comp_inl_add_comp_inr