Minlos' Theorem

Minlos' theorem: on a nuclear 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.

Proof strategy

1. Finite-dim marginals (proved in FinDimMarginals.lean): For each finite F = {f₁,...,fₙ} ⊂ E, Bochner gives μ_F on ℝⁿ with charFun = Φ(∑ tᵢfᵢ).
2. Projective family (proved in ProjectiveFamily.lean): Transport marginals to ∀ j : J, ℝ indexed by Finset E, forming an IsProjectiveMeasureFamily.
3. Kolmogorov extension (imported from KolmogorovExtension4): projectiveLimit gives measure ν on E → ℝ.
4. Measurable projection (MeasurableModification.lean): Push forward ν through a measurable map P : (E → ℝ) → WeakDual ℝ E to get μ = ν.map P.
5. CF verification: P(ω)(f) = ω(f) ν-a.e., so charFun(μ) = Φ.
6. Uniqueness: P ∘ embed = id, so μ' = (μ'.map embed).map P = ν.map P = μ.

References

• Minlos, "Generalized random processes and their extension to measures" (1959)
• Gel'fand-Vilenkin, "Generalized Functions" Vol. 4, Ch. IV, Thm 3
• Billingsley, "Convergence of Probability Measures", Thm 36.1
• Degenne-Pfaffelhuber, KolmogorovExtension4 (formalized Kolmogorov extension)

Main Theorem

theorem minlos_theorem {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsHilbertNuclear E] [TopologicalSpace.SeparableSpace E] [Nonempty E] (Φ : E → ℂ) (h_continuous : Continuous Φ) (h_positive_definite : IsPositiveDefinite Φ) (h_normalized : Φ 0 = 1) : ∃! μ : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E), ∀ (f : E), Φ f = ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ

Minlos' Theorem (existence and uniqueness): 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':

Φ(f) = ∫_{E'} exp(i ω(f)) dμ(ω)

Proof: Combine finite-dimensional Bochner (→ marginal measures), Kolmogorov extension (→ measure ν on E → ℝ), measurable projection P (→ μ = ν.map P on WeakDual ℝ E), CF verification (P(ω)(f) = ω(f) a.e.), and uniqueness (P ∘ embed = id).

References: Minlos (1959), Gel'fand-Vilenkin Vol. 4, Billingsley, Degenne-Pfaffelhuber (KolmogorovExtension4).

Derived results

theorem minlos_uniqueness {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsHilbertNuclear E] [TopologicalSpace.SeparableSpace E] [Nonempty E] {Φ : E → ℂ} (hΦ_cont : Continuous Φ) (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) {μ₁ μ₂ : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E)} (h₁ : ∀ (f : E), ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ₁ = Φ f) (h₂ : ∀ (f : E), ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ₂ = Φ f) : μ₁ = μ₂

Derived uniqueness: two probability measures with the same characteristic functional on a nuclear space must be equal.