Minlos Theorem and Gaussian Measure Construction

Uses the proven Minlos theorem from the bochner library to construct Gaussian measures. The bochner library provides:

• minlos_theorem: proven via Bochner + Kolmogorov extension
• minlos_uniqueness: derived from minlos_theorem
• IsPositiveDefinite: hermitian + nonneg PD structure (in Bochner.PositiveDefinite)

This file bridges between the GFF4D project's GFF4D.IsPositiveDefinite (nonneg only) and the bochner library's IsPositiveDefinite (hermitian + nonneg), then applies the proven Minlos theorem.

Main declarations

• minlos_gaussian_construction: Minlos + Gaussian CF → probability measure
• gaussian_measure_symmetry: covariance-preserving maps induce measure symmetries

GFF4D Positive Definiteness Lemmas

These use the GFF4D (nonneg-only) notion of positive definiteness.

theorem gaussian_rbf_pd_innerProduct {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : GFF4D.IsPositiveDefinite fun (h : H) => Complex.exp (-(1 / 2) * ↑(‖h‖ ^ 2))

Gaussian RBF kernel is positive definite on inner product spaces (GFF4D version).

theorem gaussian_positive_definite_via_embedding {E : Type u_1} {H : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : E →ₗ[ℝ] H) (covariance_form : E → E → ℝ) (h_eq : ∀ (f : E), covariance_form f f = ‖T f‖ ^ 2) : GFF4D.IsPositiveDefinite fun (f : E) => Complex.exp (-(1 / 2) * ↑(covariance_form f f))

If covariance is realized as a squared norm via a linear embedding T into a real inner product space H, then the Gaussian characteristic functional is positive definite (GFF4D sense).

Bridge lemmas: GFF4D PD → Bochner PD

The bochner library's IsPositiveDefinite requires both:

1. hermitian: φ(-x) = conj(φ(x))
2. nonneg: Re(∑ᵢⱼ cbarᵢ cⱼ φ(xᵢ - xⱼ)) ≥ 0

The GFF4D version only requires (2). For the Gaussian CF exp(-½Q(f,f)), hermiticity follows from Q(-f,-f) = Q(f,f) (which must be supplied).

theorem gff4d_to_bochner_pd {α : Type u_1} [AddGroup α] {φ : α → ℂ} (h_nonneg : GFF4D.IsPositiveDefinite φ) (h_symm : ∀ (x : α), φ (-x) = (starRingEnd ℂ) (φ x)) : IsPositiveDefinite φ

Promote GFF4D's nonneg-only PD to bochner's hermitian+nonneg PD, given an explicit symmetry proof φ(-x) = conj(φ(x)).

theorem gaussian_rbf_pd_bochner {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : IsPositiveDefinite fun (h : H) => Complex.exp (-(1 / 2) * ↑(‖h‖ ^ 2))

The Gaussian RBF kernel is positive definite in the bochner sense. The hermitian condition follows from ‖-h‖ = ‖h‖.

theorem gaussian_positive_definite_bochner {E : Type u_1} {H : Type u_2} [AddCommGroup E] [Module ℝ E] [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : E →ₗ[ℝ] H) (covariance_form : E → E → ℝ) (h_eq : ∀ (f : E), covariance_form f f = ‖T f‖ ^ 2) (h_symm : ∀ (f : E), covariance_form (-f) (-f) = covariance_form f f) : IsPositiveDefinite fun (f : E) => Complex.exp (-(1 / 2) * ↑(covariance_form f f))

Gaussian CF via embedding is PD in the bochner sense, given Q(-f,-f) = Q(f,f).

Gaussian Characteristic Functional

noncomputable def gaussianCharacteristicFunctional {E : Type u_1} (covariance_form : E → E → ℝ) (f : E) : ℂ

For Gaussian measures, the characteristic functional has the special form Φ(f) = exp(-½⟨f, Cf⟩) where C is a nuclear covariance operator.

Equations

• gaussianCharacteristicFunctional covariance_form f = Complex.exp (-(1 / 2) * ↑(covariance_form f f))

Minlos Theorem Applications

theorem minlos_gaussian_construction {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsHilbertNuclear E] [TopologicalSpace.SeparableSpace E] [Nonempty E] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : E →ₗ[ℝ] H) (covariance_form : E → E → ℝ) (h_eq : ∀ (f : E), covariance_form f f = ‖T f‖ ^ 2) (h_symm : ∀ (f : E), covariance_form (-f) (-f) = covariance_form f f) (h_zero : covariance_form 0 0 = 0) (h_continuous : Continuous fun (f : E) => covariance_form f f) : ∃ (μ : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E)), ∀ (f : E), gaussianCharacteristicFunctional covariance_form f = ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ

Application of Minlos theorem to Gaussian measures.

theorem gaussian_measure_characteristic_functional {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsHilbertNuclear E] [TopologicalSpace.SeparableSpace E] [Nonempty E] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : E →ₗ[ℝ] H) (covariance_form : E → E → ℝ) (h_eq : ∀ (f : E), covariance_form f f = ‖T f‖ ^ 2) (h_symm : ∀ (f : E), covariance_form (-f) (-f) = covariance_form f f) (h_zero : covariance_form 0 0 = 0) (h_continuous : Continuous fun (f : E) => covariance_form f f) : ∃ (μ : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E)), ∀ (f : E), ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ = gaussianCharacteristicFunctional covariance_form f

The measure constructed by Minlos theorem for a Gaussian characteristic functional indeed has that functional as its characteristic function.

Minlos Uniqueness (re-exported from bochner)

theorem minlos_gaussian_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) : μ₁ = μ₂

Uniqueness for the Gaussian CF: if two probability measures have the same Gaussian characteristic functional, they are equal.

Symmetry Transfer from Characteristic Functional to Measure

theorem gaussian_measure_symmetry {E : Type u_1} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [IsHilbertNuclear E] [TopologicalSpace.SeparableSpace E] [Nonempty E] (covariance_form : E → E → ℝ) (h_cf_cont : Continuous (gaussianCharacteristicFunctional covariance_form)) (h_cf_pd : IsPositiveDefinite (gaussianCharacteristicFunctional covariance_form)) (h_cf_norm : gaussianCharacteristicFunctional covariance_form 0 = 1) (μ : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E)) (h_char : ∀ (f : E), ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ = gaussianCharacteristicFunctional covariance_form f) (g : E →L[ℝ] E) (h_covar_symm : ∀ (f : E), covariance_form (g f) (g f) = covariance_form f f) (μ_push : MeasureTheory.ProbabilityMeasure (WeakDual ℝ E)) (h_push_char : ∀ (f : E), ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ_push = ∫ (ω : WeakDual ℝ E), Complex.exp (Complex.I * ↑(ω (g f))) ∂↑μ) : μ_push = μ

Corollary for Gaussian measures: if the covariance form is invariant under g, then the Gaussian measure is invariant under the dual action of g.