BochnerMinlos | Reservoir

Bochner's and Minlos' Theorems in Lean 4

Formal proofs of Bochner's theorem and Minlos' theorem in Lean 4 — the two foundational results characterizing when a function(al) is the Fourier transform of a probability measure — using Mathlib and KolmogorovExtension4.

Bochner's theorem

Statement: 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.

Status: 0 sorries, 0 axioms — fully proved! #print axioms bochner_theorem shows only standard Lean axioms.

The hard direction (PD implies measure) uses Gaussian regularization, avoiding Riesz-Markov-Kakutani:

Fourier positivity: For φ continuous, integrable, and positive-definite, Re(𝓕φ(ξ)) ≥ 0 for all ξ. Proved via Fejér-averaged double integrals.
Gaussian regularization: φ_ε(x) = φ(x) · exp(-ε‖x‖²) is PD (Schur product theorem) with Gaussian decay, hence L¹.
Measure construction: 𝓕φ_ε ≥ 0 gives dμ_ε = 𝓕φ_ε dλ, a probability measure with charFun(μ_ε) = φ_ε.
Weak limit: Prokhorov's theorem extracts a weakly convergent subsequence as ε → 0; the limit measure has charFun = φ.
Uniqueness: From Mathlib's Measure.ext_of_charFun.

Minlos' theorem

Statement (Lean):

theorem minlos_theorem [IsHilbertNuclear E] [SeparableSpace E] [Nonempty E]
    (Φ : E → ℂ) (h_continuous : Continuous Φ)
    (h_positive_definite : IsPositiveDefinite Φ) (h_normalized : Φ 0 = 1) :
    ∃! μ : ProbabilityMeasure (WeakDual ℝ E),
      ∀ f : E, Φ f = ∫ ω, exp (I * (ω f)) ∂μ.toMeasure

On a nuclear, separable, locally convex space E, a continuous positive-definite normalized functional Φ : E → ℂ is the characteristic functional of a unique probability measure on the topological dual E' = WeakDual ℝ E.

Status: 0 sorries, 0 axioms — fully proved! #print axioms minlos_theorem shows only standard Lean axioms.

Proof strategy:

Finite-dimensional marginals: For each finite set {f₁,...,fₙ} ⊂ E, apply Bochner's theorem to get a measure μ_F on ℝⁿ.
Projective family: Transport marginals to ∀ j : J, ℝ forming an IsProjectiveMeasureFamily.
Kolmogorov extension: The projectiveLimit (imported from KolmogorovExtension4) gives a measure ν on E → ℝ.
Measurable modification: Push forward ν through a measurable map P : (E → ℝ) → WeakDual ℝ E.
CF verification: P(ω)(f) = ω(f) ν-a.e., so charFun(μ) = Φ.
Uniqueness: P ∘ embed = id implies the representing measure is unique.

Nuclear spaces

The project formalizes two characterizations of nuclear spaces and proves the Pietsch characterization implies the Hilbertian one. The gaussian-field project independently defines NuclearSpace using the same Pietsch characterization; our IsNuclear matches it, and the bridge isHilbertNuclear_of_nuclear completes the chain to IsHilbertNuclear used by Minlos' theorem.

Hilbertian characterization (used by Minlos)

A locally convex space is nuclear if its topology is generated by a countable family of Hilbertian seminorms (satisfying the parallelogram law) with Hilbert-Schmidt inclusions between consecutive levels:

class IsHilbertNuclear (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] : Prop where
  nuclear_hilbert_embeddings :
    ∃ (p : ℕ → Seminorm ℝ E),
      (∀ n, (p n).IsHilbertian) ∧
      (WithSeminorms (fun n => p n)) ∧
      (∀ n, (p (n + 1)).IsHilbertSchmidtEmbedding (p n))

This is the characterization from Gel'fand-Vilenkin and Trèves (Ch. 50). The Hilbert-Schmidt condition means the sum ∑ q(eₖ)² is uniformly bounded over all finite p-orthonormal sequences {eₖ}.

Pietsch characterization

Every continuous seminorm p is dominated by a nuclear expansion: p(x) ≤ Σₙ |fₙ(x)| · cₙ where the fₙ are continuous linear functionals bounded by a larger seminorm q, and Σ cₙ < ∞:

def IsNuclear (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] : Prop :=
  ∀ (p : Seminorm ℝ E), Continuous p →
    ∃ (q : Seminorm ℝ E), Continuous q ∧ (∀ x, p x ≤ q x) ∧
    ∃ (f : ℕ → (E →L[ℝ] ℝ)) (c : ℕ → ℝ),
      (∀ n, 0 ≤ c n) ∧ Summable c ∧
      (∀ n x, |f n x| ≤ q x) ∧
      (∀ x, p x ≤ ∑' n, |f n x| * c n)

This is Pietsch's original definition, equivalent to requiring that the canonical maps between seminorm completions are nuclear operators.

Bridge: Pietsch implies Hilbertian

theorem isHilbertNuclear_of_nuclear [IsTopologicalAddGroup E] [ContinuousSMul ℝ E]
    (hPN : IsNuclear E)
    (q₀ : ℕ → Seminorm ℝ E) (hq₀ : WithSeminorms q₀)
    (hq₀_cont : ∀ n, Continuous (q₀ n)) :
    IsHilbertNuclear E

The bridge constructs Hilbertian seminorms via a Hilbertian lift r(x) = √(Σₖ fₖ(x)² · cₖ) from each nuclear expansion, then shows the inclusions are Hilbert-Schmidt using a Bessel inequality argument. Fully proved (0 sorries, 0 axioms).

Project structure

Three Lean libraries (~8300 lines, 0 sorries, 0 custom axioms):

Bochner — `Bochner/`

Bochner's theorem and supporting infrastructure.

File	Contents
PositiveDefinite	IsPositiveDefinite, Schur product theorem, precomp with linear maps
FejerPD	Fourier positivity: Re(𝓕φ) ≥ 0 via Fejér averaging
Main	Bochner's theorem: Gaussian regularization, Prokhorov, uniqueness
Sazonov	Sazonov topology via trace-class seminorms
TestFubini	Fubini lemmas for Gaussian regularization integrals

Minlos — `Minlos/`

Minlos' theorem, nuclear spaces, and concentration bounds.

File	Contents
NuclearSpace	IsHilbertNuclear class, Hilbertian seminorms, HS embeddings
PietschBridge	IsNuclear → IsHilbertNuclear via hilbertianLift + Bessel inequality
SazonovTightness	Sazonov CF continuity → tightness of finite-dim marginals
MinlosConcentration	Concentration theorem: Gaussian averaging, Gram matrix, Chebyshev
FinDimMarginals	Finite-dimensional marginal measures via Bochner's theorem
ProjectiveFamily	Kolmogorov projective family + extension to E → ℝ
MeasurableModification	Measurable projection P : (E → ℝ) → WeakDual ℝ E
Main	Minlos' theorem: existence + uniqueness on nuclear spaces

Test — `Test/`

Integration tests using axioms for Schwartz space properties. The gaussian-field project proves that Schwartz space is nuclear (via Hermite–Sobolev norms and the Dynin-Mityagin characterization); here we axiomatize this and other Schwartz properties to demonstrate Minlos' theorem constructing white noise on S'(ℝ).

File	Contents
WhiteNoise	White noise measure on S'(ℝ) via Minlos, bridge theorem with gaussian-field

Building

lake update
lake build

Requires Lean v4.28.0-rc1 and Mathlib.

Key Mathlib dependencies

Mathlib.Analysis.Fourier.FourierTransform — Fourier transform on inner product spaces
Mathlib.Analysis.Fourier.Inversion — Fourier inversion theorem
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform — Gaussian Fourier transform
Mathlib.MeasureTheory.Measure.Prokhorov — Prokhorov's theorem
Mathlib.MeasureTheory.Measure.CharacteristicFunction — Characteristic functions of measures
Mathlib.LinearAlgebra.Matrix.PosDef — Positive semidefinite matrices
Mathlib.Analysis.LocallyConvex.WithSeminorms — Seminorm-generated topologies
Mathlib.Topology.Algebra.Module.WeakDual — Weak-* dual spaces
KolmogorovExtension4 — Kolmogorov extension theorem (projective limits of measures)

References

Rudin, Fourier Analysis on Groups, Theorem 1.4.3
Folland, A Course in Abstract Harmonic Analysis, Chapter 4
Reed and Simon, Methods of Modern Mathematical Physics I, Section IX.9
Minlos, Generalized random processes and their extension to a measure (1959)
Gel'fand and Vilenkin, Generalized Functions Vol. 4, Chapters 3-4
Trèves, Topological Vector Spaces, Chapters 50-51
Pietsch, Nuclear Locally Convex Spaces (1972)
Degenne, Ledvinka, Marion, Pfaffelhuber, Formalization of Brownian motion in Lean (2025), arXiv:2511.20118

Author

Michael R. Douglas