Fourier-convention characteristic functions

Mathlib's characteristic function of a finite measure is t ↦ ∫ x, exp (⟪x, t⟫ * I) ∂μ, while the Fourier side of the Bochner roadmap uses the 2π convention a ↦ ∫ q, exp (-2πi⟪a, q⟫) ∂μ. This file records the conversion between these normalizations and then reuses the existing characteristic-function API to show that the Fourier-convention transform of a finite measure is continuous and positive definite.

This advances TauCetiRoadmap/OneParameterSemigroups/README.md, Part C, the positive-definite function API item asking for "a stated Fourier-convention conversion lemma between Mathlib's 2π form and the characteristic-function form" before Bochner's theorem.

Main declarations

• TauCeti.integral_fourierAtom_eq_charFun_neg_two_pi_smul: the Fourier-convention integral is charFun μ ((-2π) • a).
• TauCeti.fourierConventionCharFun_isPositiveDefiniteKernel: the Fourier-convention translation-invariant kernel of a finite measure is positive definite.

References

• Mathlib's MeasureTheory.charFun and Fourier transform convention in Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic and Mathlib.Analysis.Fourier.FourierTransform.

@[simp]

theorem TauCeti.integral_exp_neg_two_pi_inner_eq_charFun_neg_two_pi_smul {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure V} (a : V) : ∫ (q : V), Complex.exp (-(2 * ↑Real.pi * Complex.I * ↑(inner ℝ q a))) ∂μ = MeasureTheory.charFun μ ((-2 * Real.pi) • a)

The Fourier-convention integral of a finite measure, written in exponential normal form, is Mathlib's characteristic function evaluated at (-2π) • a.

theorem TauCeti.integral_fourierAtom_eq_charFun_neg_two_pi_smul {V : Type u_1} [SeminormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] {μ : MeasureTheory.Measure V} (a : V) : ∫ (q : V), fourierAtom a q ∂μ = MeasureTheory.charFun μ ((-2 * Real.pi) • a)

The Fourier-convention integral of a finite measure, written with the atom exp (-2πi⟪a, q⟫), is Mathlib's characteristic function evaluated at (-2π) • a.

theorem TauCeti.fourierConventionCharFun_isPositiveDefinite_of_star_eq_neg {W : Type u_2} [SeminormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [OpensMeasurableSpace W] {ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure ν] [StarAddMonoid W] (hstar : ∀ (x : W), star x = -x) : IsPositiveDefinite fun (a : W) => ∫ (q : W), fourierAtom a q ∂ν

The Fourier-convention transform of a finite measure is positive definite for any additive group involution that is explicitly negation. This transports the positive-definiteness of charFun μ through the -2π additive rescaling.

theorem TauCeti.fourierConventionCharFun_isPositiveDefiniteKernel {W : Type u_2} [SeminormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [OpensMeasurableSpace W] {ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure ν] : IsPositiveDefiniteKernel fun (a b : W) => ∫ (q : W), fourierAtom (a - b) q ∂ν

The translation-invariant kernel attached to the Fourier-convention transform of a finite measure is positive definite. This is the kernel form of fourierConventionCharFun_isPositiveDefinite_of_star_eq_neg, avoiding any explicit choice of involution on the domain.

theorem TauCeti.continuous_fourierConventionCharFun {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] {ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure ν] [SecondCountableTopology W] : Continuous fun (a : W) => ∫ (q : W), fourierAtom a q ∂ν

The Fourier-convention transform of a finite measure is continuous. This is just Mathlib's continuity of charFun, transported through the -2π rescaling.