GFF Measure Construction via Minlos Theorem

Constructs the Gaussian Free Field measure μ on S'(ℝ⁴) from the free covariance:

covariance → characteristic functional exp(−½⟨f,Cf⟩) → Minlos → μ

The covariance C(f,g) = ∫∫ f(x) K(x−y) g(y) dx dy with K = free propagator is shown to be symmetric, bilinear, positive semidefinite, and nuclear (via the Hilbert-Schmidt embedding from Covariance.RealForm).

Lᵖ integrability of pairings ⟨ω,f⟩ under μ is proved (not axiomatized) by showing the pushforward of μ by any pairing is a 1D Gaussian (gff_pairing_is_gaussian), then using Mathlib's memLp_id_gaussianReal.

Main definitions

• CovarianceFunction, CovarianceNuclear: covariance structure
• isGaussianGJ: characteristic functional Z[J] = exp(−½⟨J,CJ⟩)
• constructGaussianMeasureMinlosFree: the GFF measure for mass m > 0

Dependencies

No axioms declared here. Transitively uses schwartzIsHilbertNuclear, schwartzSeparableSpace and minlos_theorem (proven).

Gaussian Measures on Field Configurations

structure CovarianceFunction : Type

A covariance function on test functions that determines the Gaussian measure

• covar : TestFunctionℂ → TestFunctionℂ → ℂ

  The covariance pairing on complex test functions.

• symmetric (f g : TestFunctionℂ) : self.covar f g = (starRingEnd ℂ) (self.covar g f)
• bilinear_left (c : ℂ) (f₁ f₂ g : TestFunctionℂ) : self.covar (c • f₁ + f₂) g = c * self.covar f₁ g + self.covar f₂ g
• bilinear_right (f : TestFunctionℂ) (c : ℂ) (g₁ g₂ : TestFunctionℂ) : self.covar f (c • g₁ + g₂) = (starRingEnd ℂ) c * self.covar f g₁ + self.covar f g₂
• positive_semidefinite (f : TestFunctionℂ) : 0 ≤ (self.covar f f).re
• bounded : ∃ M > 0, ∀ (f : TestFunctionℂ), ‖self.covar f f‖ ≤ (M * ∫ (x : SpaceTime), ‖f x‖) * (∫ (x : SpaceTime), ‖f x‖ ^ 2) ^ (1 / 2)

def isCenteredGJ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

A measure is centered (has zero mean)

Equations

• isCenteredGJ dμ_config = ∀ (f : TestFunction), GJMean dμ_config f = 0

def isGaussianGJ (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : Prop

A measure is Gaussian if its generating functional has the Gaussian form. For a centered Gaussian measure, Z[J] = exp(-½⟨J, CJ⟩) where C is the covariance.

Equations

• isGaussianGJ dμ_config = (isCenteredGJ dμ_config ∧ ∀ (J : TestFunctionℂ), GJGeneratingFunctionalℂ dμ_config J = Complex.exp (-(1 / 2) * SchwingerFunctionℂ₂ dμ_config J J))

Construction via Minlos Theorem

instance instIsHilbertNuclearTestFunction : IsHilbertNuclear TestFunction

Hilbert-nuclear structure for real test functions, from schwartzIsHilbertNuclear.

instance instSeparableSpaceTestFunction : TopologicalSpace.SeparableSpace TestFunction

Separability of real test functions, from schwartzSeparableSpace.

instance instNonemptyTestFunction : Nonempty TestFunction

Nonemptiness of real test functions (the zero function).

noncomputable def constructGaussianMeasureMinlosFree (m : ℝ) [Fact (0 < m)] : MeasureTheory.ProbabilityMeasure FieldConfiguration

Specialized Minlos construction for the free field using the square-root propagator embedding.

Equations

• constructGaussianMeasureMinlosFree m = Classical.choose ⋯

noncomputable def gaussianFreeFieldFree (m : ℝ) [Fact (0 < m)] : MeasureTheory.ProbabilityMeasure FieldConfiguration

The Gaussian Free Field with mass m > 0, constructed via specialized Minlos

Equations

• gaussianFreeFieldFree m = constructGaussianMeasureMinlosFree m

@[reducible, inline]

noncomputable abbrev muGFF (m : ℝ) [Fact (0 < m)] : MeasureTheory.ProbabilityMeasure FieldConfiguration

Shorthand for the free GFF probability measure used throughout.

Equations

• muGFF m = gaussianFreeFieldFree m

theorem gff_real_characteristic (m : ℝ) [Fact (0 < m)] (f : TestFunction) : GJGeneratingFunctional (gaussianFreeFieldFree m) f = Complex.exp (-(1 / 2) * ↑(QFT.freeCovarianceFormR m f f))

Real characteristic functional of the free GFF: for real test functions f, the generating functional equals the Gaussian form with the real covariance.

Characteristic Function Bridge

These lemmas connect the GFF characteristic functional to 1D Gaussian pushforwards, proving that gaussianFreeField_pairing_memLp can be derived from first principles.

theorem gff_pairing_is_gaussian (m : ℝ) [Fact (0 < m)] (φ : TestFunction) : MeasureTheory.Measure.map ⇑(distributionPairingCLM φ) ↑(gaussianFreeFieldFree m) = ProbabilityTheory.gaussianReal 0 (QFT.freeCovarianceFormR m φ φ).toNNReal

The pushforward of the GFF measure by pairing with a test function is a 1D Gaussian. Proven via characteristic functions and Lévy's uniqueness theorem.

theorem gaussianFreeField_pairing_memLp (m : ℝ) [Fact (0 < m)] (φ : TestFunction) (p : ENNReal) (hp : p ≠ ⊤) : MeasureTheory.MemLp (⇑(distributionPairingCLM φ)) p ↑(gaussianFreeFieldFree m)

Fernique's Theorem for GFF: Every distribution pairing has finite moments of all orders.

This is proven using characteristic functions:

1. gff_pairing_is_gaussian shows the pushforward is a 1D Gaussian
2. Gaussian measures on ℝ have finite moments (Mathlib's memLp_id_gaussianReal)
3. Pull back through the measurable pairing map

Proven via the characteristic function bridge.

theorem gff_pairing_square_integrable (m : ℝ) [Fact (0 < m)] (φ : TestFunction) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => (distributionPairingCLM φ) ω ^ 2) ↑(gaussianFreeFieldFree m)

The GFF pairing has an integrable square (is in L²). This follows from the fact that the pushforward is a Gaussian measure, and Gaussian measures have finite moments of all orders.

theorem gff_second_moment_eq_covariance (m : ℝ) [Fact (0 < m)] (φ : TestFunction) : ∫ (ω : FieldConfiguration), (distributionPairingCLM φ) ω ^ 2 ∂↑(gaussianFreeFieldFree m) = QFT.freeCovarianceFormR m φ φ

The second moment of the GFF pairing equals the covariance form. This follows from the fact that the pushforward is a Gaussian with variance equal to the covariance form, and for centered Gaussians, variance = second moment.

theorem freeCovarianceFormR_gaussian_cf_pd (m : ℝ) [Fact (0 < m)] : IsPositiveDefinite fun (f : TestFunction) => Complex.exp (-(1 / 2) * ↑(QFT.freeCovarianceFormR m f f))

The Gaussian CF with the free covariance is positive definite, via the square-root propagator embedding into a Hilbert space.

noncomputable def freeCovarianceForm (m : ℝ) [Fact (0 < m)] : MinlosAnalytic.CovarianceForm

The free covariance form as a MinlosAnalytic.CovarianceForm structure.

Equations

• freeCovarianceForm m = { Q := QFT.freeCovarianceFormR m, symm := ⋯, psd := ⋯, cont_diag := ⋯, add_left := ⋯, smul_left := ⋯, gaussian_cf_pd := ⋯ }

theorem gaussianFreeField_free_centered (m : ℝ) [Fact (0 < m)] : isCenteredGJ (gaussianFreeFieldFree m)

The GFF has zero mean: the measure is centered.

Proof: The characteristic functional gff_real_characteristic shows that Z[f] = exp(-½⟨f,Cf⟩) depends only on the quadratic form freeCovarianceFormR m f f, which is symmetric under f ↦ -f. By integral_neg_invariance, the measure is invariant under ω ↦ -ω. From this negation invariance: GJMean μ φ = ∫ ⟨ω,φ⟩ dμ = ∫ ⟨-ω,φ⟩ dμ = -∫ ⟨ω,φ⟩ dμ implying GJMean μ φ = 0.

theorem gaussianFreeField_pairing_expSq_integrable (m : ℝ) [Fact (0 < m)] (φ : TestFunction) : ∃ (α : ℝ), 0 < α ∧ MeasureTheory.Integrable (fun (ω : FieldConfiguration) => Real.exp (α * (distributionPairingCLM φ) ω ^ 2)) ↑(gaussianFreeFieldFree m)

Fernique's Theorem for GFF (exponential form): For every real test function φ, there exists α > 0 such that exp(α * ⟨ω, φ⟩²) is integrable under the free GFF measure.

This follows from gff_pairing_is_gaussian which shows the pushforward is a 1D Gaussian, combined with Mathlib's IsGaussian.exists_integrable_exp_sq (Fernique's theorem).

theorem gaussian_pairing_square_integrable_real (m : ℝ) [Fact (0 < m)] (φ : TestFunction) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => distributionPairing ω φ ^ 2) ↑(gaussianFreeFieldFree m)

For real test functions, the square of the Gaussian pairing is integrable under the free Gaussian Free Field measure. This is the diagonal (f = g) case needed for establishing two-point integrability.