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.

The file also bridges Mathlib's Fourier transform 𝓕 to the Fourier atom, and it carries the measure-uniqueness theorem — the uniqueness half of Bochner's theorem — consumed by BochnerTheorem.lean. The convention-free continuity of 𝓕 and 𝓕⁻ lives in TauCeti.Analysis.Fourier.Continuous.

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.fourier_eq_integral_fourierAtom_mul: the Fourier transform 𝓕 F is the integral of F against the Fourier atom.
• TauCeti.posSemidef_fourierConventionCharFun_sub: the Fourier-convention translation-invariant kernel of a finite measure is positive definite.
• TauCeti.Measure.ext_of_forall_integral_fourierAtom_eq: a finite measure is determined by its Fourier-convention transform — the uniqueness half of Bochner's theorem.

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.

Not a @[simp] lemma: simp already proves it — fourierAtom_apply and neg_mul rewrite the left-hand side into that of the simp lemma integral_exp_neg_two_pi_inner_eq_charFun_neg_two_pi_smul, which the simpNF linter reports as a duplicate if this statement is also tagged @[simp].

theorem TauCeti.neg_two_pi_ne_zero : -2 * Real.pi ≠ 0

The scaling constant -2π of the Fourier convention is nonzero.

theorem TauCeti.fourier_eq_integral_fourierAtom_mul {U : Type u_2} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [FiniteDimensional ℝ U] [MeasurableSpace U] [BorelSpace U] (F : U → ℂ) (ξ : U) : FourierTransform.fourier F ξ = ∫ (v : U), fourierAtom ξ v * F v

The Fourier transform written as the integral against the Fourier atom.

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.posSemidef_fourierConventionCharFun_sub {W : Type u_2} [SeminormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [OpensMeasurableSpace W] {ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure ν] : Matrix.PosSemidef 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.

theorem TauCeti.Measure.ext_of_forall_integral_fourierAtom_eq {W : Type u_3} [NormedAddCommGroup W] [InnerProductSpace ℝ W] [MeasurableSpace W] [BorelSpace W] [SecondCountableTopology W] [CompleteSpace W] {μ ν : MeasureTheory.Measure W} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : ∀ (v : W), ∫ (q : W), fourierAtom v q ∂μ = ∫ (q : W), fourierAtom v q ∂ν) : μ = ν

Uniqueness half of Bochner's theorem. Two finite Borel measures with the same Fourier-convention transform coincide; this is Mathlib's characteristic-function uniqueness theorem, transported through the -2π rescaling. Stated on any complete second-countable real inner-product space; no finite-dimensionality is needed.