Characteristic functions as positive-definite functions

This file connects the quadratic-form positivity calculation for characteristic functions to Tau Ceti's generic positive-definite-function predicate. If the involution on an additive group is negation, then Mathlib's characteristic function MeasureTheory.charFun μ of a finite measure is TauCeti.IsPositiveDefinite.

Together with Mathlib's continuity theorem for characteristic functions, this gives the "finite measure's Fourier transform is continuous positive-definite" bridge lemma requested in Part C of the OneParameterSemigroups roadmap, before the harder converse direction of Bochner's theorem.

Main declarations

• TauCeti.charFun_isPositiveDefinite_of_star_eq_neg: charFun μ is positive definite for any explicit star = - involution.
• TauCeti.continuous_charFun_and_isPositiveDefinite_of_star_eq_neg: the paired continuity and positive-definiteness package.
• TauCeti.isPositiveDefiniteSub_charFun: charFun μ is positive definite in the subtraction form TauCeti.IsPositiveDefiniteSub, with no choice of involution.

theorem TauCeti.charFun_isPositiveDefinite_of_star_eq_neg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [StarAddMonoid E] (hstar : ∀ (x : E), star x = -x) : IsPositiveDefinite (MeasureTheory.charFun μ)

The characteristic function of a finite measure is positive definite for any additive-group involution that is explicitly negation. This is the generic-predicate form of charFun_fintype_sum_mul_conj_nonneg, using F (vᵢ + star vⱼ) = charFun μ (vᵢ - vⱼ).

theorem TauCeti.isPositiveDefiniteSub_charFun {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] : IsPositiveDefiniteSub (MeasureTheory.charFun μ)

The characteristic function of a finite measure is positive definite in the subtraction form: ∑ i, ∑ j, c i * conj (c j) * charFun μ (v i - v j) is nonnegative.

theorem TauCeti.continuous_charFun_and_isPositiveDefinite_of_star_eq_neg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] [StarAddMonoid E] (hstar : ∀ (x : E), star x = -x) : Continuous (MeasureTheory.charFun μ) ∧ IsPositiveDefinite (MeasureTheory.charFun μ)

The characteristic function of a finite measure on a second-countable real inner product space is continuous and positive definite, provided the chosen involution is negation. This is the forward bridge toward Bochner's theorem in the language of TauCeti.IsPositiveDefinite.