Documentation

LeanPool.OSforGFF.Schwinger.GaussianMoments

Gaussian Moments and n-Point Integrability #

This file proves that Gaussian Free Field measures have finite moments of all orders, establishing integrability of n-point correlation functions for arbitrary n.

Main Results: #

Key Insight: Gaussian measures on nuclear spaces have finite polynomial moments of all orders. Since each pairing ⟨ω, f⟩ is linear in ω, their n-fold product is a polynomial of degree n, hence integrable.

Proof Strategy:

  1. Base Cases: n = 0, 1, 2 (trivial, linear functional, covariance bound)
  2. Inductive Step: Use Gaussian moment properties and Cauchy-Schwarz
  3. Nuclear Foundation: Leverage nuclear covariance structure

This generalizes gaussian_pairing_product_integrable_free_core to arbitrary n, providing a unified foundation for all Schwinger function computations.

n-Point Integrability for Gaussian Free Fields #

source
theorem GaussianMoments.gaussian_complex_pairing_abs_sq_integrable (m : ℝ) [Fact (0 < m)] (φ : TestFunctionℂ) :
MeasureTheory.Integrable (fun (ω : FieldConfiguration) => ‖distributionPairingℂReal ω φ‖ ^ 2) ↑(gaussianFreeFieldFree m)

Auxiliary lemma: the complex pairing has an integrable square under the free GFF measure. This is the complex analogue of gaussian_pairing_square_integrable_real and will serve as the base estimate for higher Gaussian moments.

source
theorem gaussian_pairing_product_integrable_free_2point (m : ℝ) [Fact (0 < m)] (φ ψ : TestFunctionℂ) :
MeasureTheory.Integrable (fun (ω : FieldConfiguration) => distributionPairingℂReal ω φ * distributionPairingℂReal ω ψ) ↑(gaussianFreeFieldFree m)

Foundation: The original 2-point case implemented directly. This provides the base case for the general n-point theorem.

source
theorem covariance_bilinear_from_general (m : ℝ) [Fact (0 < m)] :
CovarianceBilinear (gaussianFreeFieldFree m)

Corollary: The complex covariance is well-defined via the general integrability.

Implementation Notes #

Current Status: #

  1. Structure: Complete framework for n-point integrability
  2. Base Cases: n = 0, 1 implemented; n = 2 reduces to core lemma
  3. Inductive Step: Outlined using Gaussian moment theory
  4. Applications: Schwinger functions and covariance bilinearity derived

Next Steps: #

  1. Implement n = 1 case: Use Schwartz space bounds + nuclear structure
  2. Implement n = 2 case: Use one of three approaches:
    • Nuclear/Minlos: Leverage explicit construction
    • Characteristic Function: Use Gaussian 2D distribution
    • Hilbert Embedding: Use square-root propagator embedding
  3. Complete n ≥ 3: Use Gaussian finite moment theorem + induction

Mathematical Foundation: #

Key Insight: Nuclear covariance ⟹ all polynomial moments finite Strategy: Reduce to established Gaussian measure theory Connection: Links constructive QFT (Minlos) to abstract theory (OS axioms)

This approach provides a clean separation between: