Bochner's Theorem

Bochner's theorem states that a continuous function φ : V → ℂ on a finite-dimensional real inner product space is positive definite with φ(0) = 1 if and only if it is the characteristic function of a unique probability measure on V.

Proof strategy

We prove the hard direction (PD → measure) via Gaussian regularization, avoiding the Riesz-Markov-Kakutani theorem entirely:

1. Phase 1 (pd_l1_fourier_nonneg): An L¹ positive-definite function has a nonneg real Fourier transform. Proved by testing the PD double integral against explicit shifted Gaussians g(x) = exp(-a‖x‖² - i⟨ξ₀,x⟩). Since |ĝ(ξ)|² forms a Dirac sequence as a → 0, continuity of φ̂ (from Riemann-Lebesgue) forces φ̂(ξ₀) ≥ 0 at every point.

2. Phase 2 (gaussian_regularization): Define φ_ε(x) = φ(x) · exp(-ε‖x‖²). By Schur (pointwise product of PD is PD), φ_ε is PD. Gaussian decay guarantees φ_ε ∈ L¹.

3. Phase 3 (measure_of_pd_l1): Apply Phase 1 to get φ̂_ε ≥ 0, then define dμ_ε = φ̂_ε dλ. Since ∫ φ̂_ε = φ_ε(0) = 1, this is a probability measure. By Fourier inversion, charFun(μ_ε) = φ_ε.

4. Phase 4 (tightness_from_charfun): As ε → 0, charFun(μ_ε)(x) → φ(x) pointwise. Tightness of {μ_ε} follows from the standard bound μ({‖x‖ > R}) ≤ C ∫{‖ξ‖≤δ} (1 - Re(φ̂_ε(ξ))) dξ → 0, using continuity of φ at 0. Prokhorov's theorem (in Mathlib) extracts a weakly convergent subsequence μ{ε_k} → μ. Testing against x ↦ exp(i⟨ξ,x⟩) shows charFun(μ) = φ.

5. Phase 5 (Measure.ext_of_charFun): Uniqueness is already in Mathlib.

Main results

• bochner_theorem: the full theorem
• pd_l1_fourier_nonneg: L¹ PD ⟹ nonneg Fourier transform (Phase 1)

References

• S. Bochner, "Monotone Funktionen, Stieltjessche Integrale und harmonische Analyse", Math. Annalen 108 (1933), 378–410
• W. Rudin, Fourier Analysis on Groups, Wiley (1962), Theorem 1.4.3
• G.B. Folland, A Course in Abstract Harmonic Analysis, CRC Press (2016), §4.2

Phase 1: L¹ positive-definite functions have nonneg Fourier transform

The proof uses explicit shifted Gaussians rather than abstract Plancherel.

Given φ ∈ L¹ with φ positive-definite, we want φ̂(ξ₀) ≥ 0 for each ξ₀.

Test the PD condition with g_a(x) = exp(-a‖x‖²) exp(-i⟨ξ₀,x⟩): 0 ≤ ∫∫ gbar_a(x) g_a(y) φ(x-y) dx dy = ∫ |ĝ_a(ξ)|² φ̂(ξ) dξ

Since ĝ_a is an explicit Gaussian (Mathlib: fourier_gaussian_innerProductSpace'), |ĝ_a|² is a Gaussian centered at ξ₀ with width ~ 1/√a. As a → 0⁺, this concentrates at ξ₀. Since φ̂ is continuous (Riemann-Lebesgue), the integral converges to φ̂(ξ₀) · (const), giving φ̂(ξ₀) ≥ 0.

Phase 1.5: Characteristic functions are positive definite

The "forward" direction of Bochner: the characteristic function of any finite measure is positive definite. This gives us PD of the Gaussian as a corollary: exp(-ε‖x‖²) is the charFun of a Gaussian measure.

theorem isPositiveDefinite_charFun {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] : IsPositiveDefinite fun (t : V) => MeasureTheory.charFun μ t

Forward Bochner: the characteristic function of any finite measure is PD.

Proof: charFun(μ)(t) = ∫ exp(i⟨x,t⟩) dμ(x). So ∑ᵢⱼ cbarᵢcⱼ charFun(tᵢ-tⱼ) = ∫ |∑ₖ cₖ exp(i⟨x,tₖ⟩)|² dμ(x) ≥ 0.

The key steps are: (1) swap finite sum and integral, (2) recognize the integrand as a norm squared.

theorem isPositiveDefinite_mul_charFun {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MeasurableSpace V] [BorelSpace V] {φ : V → ℂ} (hpd : IsPositiveDefinite φ) (μ : MeasureTheory.Measure V) [MeasureTheory.IsFiniteMeasure μ] : IsPositiveDefinite fun (t : V) => φ t * MeasureTheory.charFun μ t

Pointwise product of a PD function and the characteristic function of a finite measure is PD. This is a "continuous Schur product" — the same algebraic trick as isPositiveDefinite_charFun but with modified coefficients d_k(x) = c_k · exp(-i⟨x, t_k⟩) absorbed into the PD condition.

theorem isPositiveDefinite_gaussian {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (ε : ℝ) (hε : 0 < ε) : IsPositiveDefinite fun (x : V) => Complex.exp (-↑ε * ↑(‖x‖ ^ 2))

The Gaussian function x ↦ exp(-ε‖x‖²) is positive definite.

Proved by showing it is the characteristic function of a centered Gaussian measure with variance 1/(2ε).

Phase 2: Gaussian regularization

φ_ε(x) = φ(x) · exp(-ε‖x‖²) is PD (Schur) and L¹ (bounded × Gaussian).

noncomputable def gaussianRegularize {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (ε : ℝ) : V → ℂ

The Gaussian-regularized function.

Equations

• gaussianRegularize φ ε x = φ x * Complex.exp (-↑ε * ↑(‖x‖ ^ 2))

theorem gaussianRegularize_pd {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (ε : ℝ) (hε : 0 < ε) : IsPositiveDefinite (gaussianRegularize φ ε)

φ_ε is positive definite (Schur product of PD functions).

Direct proof via the Fourier representation of the Gaussian, avoiding the general Schur product theorem.

exp(-ε‖xᵢ-xⱼ‖²) = ∫ exp(2πi⟨ξ,xᵢ-xⱼ⟩) g(ξ) dξ where g ≥ 0

So ∑ᵢⱼ cbarᵢcⱼ φ(xᵢ-xⱼ) exp(-ε‖xᵢ-xⱼ‖²) = ∫ g(ξ) [∑ᵢⱼ (cᵢ e^{2πi⟨xᵢ,ξ⟩})* (cⱼ e^{2πi⟨xⱼ,ξ⟩}) φ(xᵢ-xⱼ)] dξ

The inner sum has .re ≥ 0 by PD of φ, and g ≥ 0, so the integral ≥ 0.

theorem gaussianRegularize_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hcont : Continuous φ) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.Integrable (gaussianRegularize φ ε) MeasureTheory.volume

φ_ε is integrable (φ is bounded by φ(0), times Gaussian decay).

theorem gaussianRegularize_zero {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (ε : ℝ) : gaussianRegularize φ ε 0 = φ 0

φ_ε(0) = φ(0).

theorem gaussianRegularize_tendsto {V : Type u_1} [NormedAddCommGroup V] (φ : V → ℂ) (x : V) : Filter.Tendsto (fun (ε : ℝ) => gaussianRegularize φ ε x) (nhdsWithin 0 (Set.Ioi 0)) (nhds (φ x))

φ_ε → φ pointwise as ε → 0⁺.

Phase 1 proof: Re(𝓕φ(ξ)) ≥ 0 for L¹ PD functions

The proof approximates 𝓕φ(ξ) by 𝓕(φ_ε)(ξ) where φ_ε = φ·exp(-ε‖·‖²). By DCT, 𝓕(φ_ε)(ξ) → 𝓕(φ)(ξ) as ε → 0⁺. We show Re(𝓕(φ_ε)(ξ)) ≥ 0 for each ε > 0 via Fejér sums using the discrete PD condition.

The Fejér sum argument: For ψ PD continuous integrable with Gaussian decay, take N lattice points in each direction. The PD double sum with Fourier coefficients gives a Fejér-weighted Riemann sum S_N with Re(S_N) ≥ 0. As the lattice refines and grows, S_N → 𝓕ψ(ξ), giving Re(𝓕ψ(ξ)) ≥ 0.

theorem pd_l1_fourier_re_nonneg_ax (V : Type u_2) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (ξ : V) : 0 ≤ (FourierTransform.fourier φ ξ).re

The Fourier transform of a continuous integrable positive-definite function on a finite-dimensional real inner product space has nonneg real part.

Proved in Bochner.FejerPD via Fejér-weighted PD sums. Refs: Rudin, Theorem 1.4.3; Folland, §4.2, Lemma 4.8.

theorem pd_l1_fourier_re_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (ξ : V) : 0 ≤ (FourierTransform.fourier φ ξ).re

The real part of the Fourier transform of an L¹ PD function is nonneg. Ref: Folland, A Course in Abstract Harmonic Analysis, §4.2, Lemma 4.8.

theorem pd_l1_fourier_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (ξ : V) : 0 ≤ (FourierTransform.fourier φ ξ).re ∧ (FourierTransform.fourier φ ξ).im = 0

An L¹ positive-definite function has a nonneg real Fourier transform. Continuity of φ̂ (from Riemann-Lebesgue) means this holds everywhere, not just a.e.

theorem pd_l1_fourier_real_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (ξ : V) : FourierTransform.fourier φ ξ = ↑(FourierTransform.fourier φ ξ).re ∧ 0 ≤ (FourierTransform.fourier φ ξ).re

The Fourier transform of an L¹ PD function is real and nonneg.

Phase 3: Construct probability measures from L¹ PD functions

Given φ ∈ L¹ PD with φ(0) = 1, define dμ = φ̂ · dλ. Since φ̂ ≥ 0 (Phase 1) and ∫ φ̂ = φ(0) = 1 (Fourier inversion at 0), μ is a probability measure. By Fourier inversion, charFun(μ) = φ.

theorem measure_of_pd_l1 {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hint : MeasureTheory.Integrable φ MeasureTheory.volume) (hcont : Continuous φ) (hnorm : φ 0 = 1) (hint_ft : MeasureTheory.Integrable (FourierTransform.fourier φ) MeasureTheory.volume) : ∃ (μ : MeasureTheory.ProbabilityMeasure V), ∀ (ξ : V), MeasureTheory.charFun (↑μ) ξ = φ ξ

Given an L¹ PD function with φ(0) = 1, there exists a probability measure whose characteristic function equals φ.

Key idea: define ψ(x) = φ(2πx) to absorb the 2π convention difference between charFun (uses e^{i⟪x,t⟫}) and 𝓕 (uses e^{-2πi⟪x,ξ⟫}). Then dμ = 𝓕ψ · dλ is a probability measure with charFun(μ) = φ.

Phase 4: Tightness and weak limit

The family {μ_ε} is tight because: μ_ε({‖x‖ > R}) ≤ (2/R²) ∫_{‖ξ‖≤δ} (1 - Re(charFun(μ_ε)(ξ))) dξ

Since charFun(μ_ε) = φ_ε → φ and φ is continuous at 0, the right side → 0 uniformly in ε as R → ∞.

Prokhorov's theorem (Mathlib: isCompact_closure_of_isTightMeasureSet) extracts a weakly convergent subsequence. Testing the limit against x ↦ exp(i⟨ξ,x⟩) identifies charFun(μ) = φ.

theorem gaussianRegularize_ft_integrable {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hcont : Continuous φ) (ε : ℝ) (hε : 0 < ε) : MeasureTheory.Integrable (FourierTransform.fourier (gaussianRegularize φ ε)) MeasureTheory.volume

The Fourier transform of a Gaussian-regularized PD function is integrable. Proof: 𝓕(φ_ε) ≥ 0 (from PD), and for each t > 0 the Parseval/Fubini identity gives ∫ (𝓕 φ_ε) * g_t = ∫ φ_ε * (𝓕 g_t), bounded by ‖φ_ε‖∞ * ‖𝓕 g_t‖₁ = (φ 0).re. Monotone convergence (g_t ↗ 1) gives ∫⁻ ‖𝓕 φ_ε‖ ≤ (φ 0).re < ∞. Ref: Folland, A Course in Abstract Harmonic Analysis, 4.2.

theorem gaussianRegularize_measures_tight {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hpd : IsPositiveDefinite φ) (hcont : Continuous φ) (hnorm : φ 0 = 1) : MeasureTheory.IsTightMeasureSet {μ : MeasureTheory.Measure V | ∃ (ε : ℝ), 0 < ε ∧ ε ≤ 1 ∧ ∃ (_ : MeasureTheory.IsProbabilityMeasure μ), ∀ (ξ : V), MeasureTheory.charFun μ ξ = gaussianRegularize φ ε ξ}

The family of measures constructed from Gaussian regularization is tight. For each ε > 0, μ_ε is the probability measure with charFun(μ_ε) = φ_ε. The tightness bound follows from: for any probability measure μ, μ({|⟪a,x⟫| > r}) ≤ C · r · ∫_{-2/r}^{2/r} (1 - Re(charFun μ (t·a))) dt (Mathlib: measureReal_abs_inner_gt_le_integral_charFun). Since charFun(μ_ε) = φ_ε → φ uniformly on compacts and φ is continuous at 0 with φ(0) = 1, the RHS → 0 uniformly in ε as r → ∞. Ref: Folland, §4.2, proof of Theorem 4.15.

Phase 5: Uniqueness (from Mathlib)

MeasureTheory.Measure.ext_of_charFun already proves that charFun determines the measure uniquely.

Main Theorem

theorem bochner_theorem {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] (φ : V → ℂ) (hcont : Continuous φ) (hpd : IsPositiveDefinite φ) (hnorm : φ 0 = 1) : ∃! μ : MeasureTheory.ProbabilityMeasure V, ∀ (ξ : V), MeasureTheory.charFun (↑μ) ξ = φ ξ

Bochner's Theorem. A continuous positive-definite function φ : V → ℂ with φ(0) = 1 on a finite-dimensional real inner product space is the characteristic function of a unique probability measure on V.

This is the finite-dimensional version. The infinite-dimensional generalization (Bochner-Minlos) additionally requires nuclearity of the domain space.