A finite measure's characteristic function is positive definite

This file proves the "easy" (necessary) direction of Bochner's theorem: the characteristic function charFun μ of a finite measure μ on a real inner product space E is a positive-definite function. Concretely, for every finite family (cᵢ, tᵢ) the Hermitian form

∑ᵢ ∑ⱼ cᵢ · conj cⱼ · charFun μ (tᵢ - tⱼ)

is a nonnegative real number (charFun_sum_mul_conj_nonneg), equivalently the matrix (charFun μ (tᵢ - tⱼ))ᵢⱼ is positive semidefinite (posSemidef_charFun). The proof is the classical computation: the Hermitian form equals the honest integral

∫ y, ‖∑ᵢ cᵢ · exp (⟪y, tᵢ⟫ * I)‖² ∂μ

of a nonnegative integrand (charFun_sum_mul_conj_eq_integral), because exp (⟪y, tᵢ⟫ * I) · conj (exp (⟪y, tⱼ⟫ * I)) = exp (⟪y, tᵢ - tⱼ⟫ * I) makes the double sum factor through a squared modulus.

This is the roadmap's bridge lemma pd_quadratic_form_of_measure (TauCetiRoadmap/OneParameterSemigroups/README.md, Part C — "Positive-definite functions and Bochner's theorem", the API to develop bullet "a finite measure's Fourier transform is continuous positive-definite"). It is stated directly on Mathlib's MeasureTheory.charFun, so it needs no positive-definiteness predicate; it is exactly the half of Bochner's theorem that is provable without the harder measure-extraction (Riesz–Markov / Lévy–Prokhorov) machinery.

charFun and innerProbChar are from Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean; positive semidefiniteness of complex matrices is Mathlib's Matrix.PosSemidef.

theorem TauCeti.charFun_sum_mul_conj_eq_integral {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_2} (s : Finset ι) (c : ι → ℂ) (t : ι → E) : ∑ i ∈ s, ∑ j ∈ s, c i * (starRingEnd ℂ) (c j) * MeasureTheory.charFun μ (t i - t j) = ↑(∫ (y : E), Complex.normSq (∑ i ∈ s, c i * Complex.exp (↑(inner ℝ y (t i)) * Complex.I)) ∂μ)

The Hermitian form of charFun μ over a finite family (cᵢ, tᵢ) equals the integral of a squared modulus. This is the engine behind positive-definiteness: the right-hand side is the integral of a manifestly nonnegative function.

theorem TauCeti.charFun_sum_mul_conj_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_2} (s : Finset ι) (c : ι → ℂ) (t : ι → E) : 0 ≤ ∑ i ∈ s, ∑ j ∈ s, c i * (starRingEnd ℂ) (c j) * MeasureTheory.charFun μ (t i - t j)

The Hermitian form of charFun μ over a finite family (cᵢ, tᵢ) is a nonnegative real: charFun μ is a positive-definite function. This is pd_quadratic_form_of_measure.

theorem TauCeti.charFun_fintype_sum_mul_conj_nonneg {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] {ι : Type u_2} [Fintype ι] (c : ι → ℂ) (t : ι → E) : 0 ≤ ∑ i : ι, ∑ j : ι, c i * (starRingEnd ℂ) (c j) * MeasureTheory.charFun μ (t i - t j)

The Fintype-indexed form of positive-definiteness: summing over all of a finite index type.

theorem TauCeti.posSemidef_charFun {E : Type u_1} [SeminormedAddCommGroup E] [InnerProductSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure μ] : Matrix.PosSemidef fun (x y : E) => MeasureTheory.charFun μ (x - y)

The subtraction kernel (x, y) ↦ charFun μ (x - y) of a finite measure is positive semidefinite: the matrix reformulation of the positive-definiteness of charFun μ.