Minlos Analyticity — Symmetry and Moments for Gaussian Measures

This file provides infrastructure for Gaussian measures constructed via Minlos' theorem:

• CovarianceForm: Real symmetric bilinear form for covariance
• negMap, integral_neg_invariance: Symmetry under sign flip (uses Minlos uniqueness)
• moment_zero_from_realCF: Zero mean from characteristic functional symmetry

Contents

This file provides infrastructure for Gaussian measures via Minlos. No axioms declared here.

structure MinlosAnalytic.CovarianceForm : Type

A real symmetric, positive semidefinite covariance form on real test functions, together with a proof that the associated Gaussian characteristic functional exp(-½Q(f,f)) is positive definite (in the bochner sense).

• Q : TestFunction → TestFunction → ℝ

  The real covariance bilinear form.

• symm (f g : TestFunction) : self.Q f g = self.Q g f
• psd (f : TestFunction) : 0 ≤ self.Q f f
• cont_diag : Continuous fun (f : TestFunction) => self.Q f f
• add_left (f₁ f₂ g : TestFunction) : self.Q (f₁ + f₂) g = self.Q f₁ g + self.Q f₂ g
• smul_left (c : ℝ) (f g : TestFunction) : self.Q (c • f) g = c * self.Q f g
• gaussian_cf_pd : IsPositiveDefinite fun (f : TestFunction) => Complex.exp (-(1 / 2) * ↑(self.Q f f))

noncomputable def MinlosAnalytic.negMap : FieldConfiguration → FieldConfiguration

The negation map on field configurations: T(ω) = -ω

Equations

• MinlosAnalytic.negMap ω = -ω

theorem MinlosAnalytic.negMap_measurable : Measurable negMap

The negation map is measurable w.r.t. the cylinder σ-algebra.

theorem MinlosAnalytic.integral_neg_invariance [IsHilbertNuclear TestFunction] [TopologicalSpace.SeparableSpace TestFunction] [Nonempty TestFunction] [IsTopologicalAddGroup TestFunction] [ContinuousSMul ℝ TestFunction] (C : CovarianceForm) (μ : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_realCF : ∀ (f : TestFunction), ∫ (ω : FieldConfiguration), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ = Complex.exp (-(1 / 2) * ↑(C.Q f f))) (f : FieldConfiguration → ℂ) : MeasureTheory.Integrable f ↑μ → ∫ (ω : FieldConfiguration), f ω ∂↑μ = ∫ (ω : FieldConfiguration), f (-ω) ∂↑μ

Symmetry under global sign flip induced by the real Gaussian CF. Uses Minlos uniqueness from the bochner library.

theorem MinlosAnalytic.moment_zero_from_realCF [IsHilbertNuclear TestFunction] [TopologicalSpace.SeparableSpace TestFunction] [Nonempty TestFunction] [IsTopologicalAddGroup TestFunction] [ContinuousSMul ℝ TestFunction] (C : CovarianceForm) (μ : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_realCF : ∀ (f : TestFunction), ∫ (ω : FieldConfiguration), Complex.exp (Complex.I * ↑(ω f)) ∂↑μ = Complex.exp (-(1 / 2) * ↑(C.Q f f))) (a : TestFunction) (hInt1 : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => ↑(ω a)) ↑μ) : ∫ (ω : FieldConfiguration), ↑(ω a) ∂↑μ = 0

Zero mean from the real Gaussian characteristic functional, via symmetry and L¹.