Gaussianity Verification

Identifies S₂(f,g) = C(f,g) via the identity theorem, using OS0's derivative interchange. From Z[tf+sg] = exp(−½ Q(tf+sg, tf+sg)):

• ∂²/∂t∂s|₀ via Gaussian formula gives −Q(f,g)
• ∂²/∂t∂s|₀ via integral interchange (OS0) gives −S₂(f,g)
• Hence S₂(f,g) = Q(f,g) = freeCovarianceℂ(f,g)

This imports OS0 because it uses the proved analyticity to justify the derivative interchange, not because of OS0-specific infrastructure.

Main results

• gff_two_point_equals_covarianceℂ_free: S₂(f,g) = freeCovarianceℂ(f,g)
• isGaussianGJ_gaussianFreeField_free: the free GFF is Gaussian

Main Results

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

For the Gaussian Free Field measure, the product of two complex pairings with test functions is integrable. Uses the direct 2-point theorem from GaussianMoments.

Core Theorems

The proofs use OS0's derivative interchange machinery:

1. gff_real_characteristic gives Z[f] = exp(-½ Q(f,f)) for real f
2. gaussianFreeField_satisfies_OS0 gives analyticity of Z
3. hasFDerivAt_integral_of_dominated_of_fderiv_le (used in OS0) gives derivative interchange
4. Computing ∂²Z/∂t∂s|₀ two ways (Gaussian formula vs integral) gives S₂ = Q

theorem GFFIsGaussian.freeCovarianceFormR_bilinear_expand (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (t s : ℝ) : QFT.freeCovarianceFormR m (t • f + s • g) (t • f + s • g) = t ^ 2 * QFT.freeCovarianceFormR m f f + 2 * t * s * QFT.freeCovarianceFormR m f g + s ^ 2 * QFT.freeCovarianceFormR m g g

Bilinearity expansion of Q(tf+sg, tf+sg). Q(tf+sg, tf+sg) = t²Q(f,f) + 2ts Q(f,g) + s²Q(g,g)

theorem GFFIsGaussian.gff_cf_two_testfunctions (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (t s : ℝ) : GJGeneratingFunctional (gaussianFreeFieldFree m) (t • f + s • g) = Complex.exp (-(1 / 2) * (↑t ^ 2 * ↑(QFT.freeCovarianceFormR m f f) + 2 * ↑t * ↑s * ↑(QFT.freeCovarianceFormR m f g) + ↑s ^ 2 * ↑(QFT.freeCovarianceFormR m g g)))

The Gaussian CF formula for two test functions.

OS0-Based Derivative Machinery

The following lemmas use OS0's analyticity to compute mixed derivatives.

theorem GFFIsGaussian.gff_two_param_analytic (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : AnalyticOn ℂ (fun (z : Fin 2 → ℂ) => GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (z 0 • toComplex f + z 1 • toComplex g)) Set.univ

OS0 specialized to two test functions gives analyticity of Z[tf + sg] in (t,s) ∈ ℂ²

OS0-Based Complex Extension via Identity Theorem

The key insight is that we can extend from real to complex test functions using:

1. OS0 gives analyticity of Z[z₀f + z₁g] in (z₀, z₁) ∈ ℂ²
2. For real parameters, we have the Gaussian formula
3. The Gaussian formula defines an entire function of (z₀, z₁)
4. By the identity theorem (applied twice in 1D), the two analytic functions agree everywhere

This eliminates the need for twoD_line_from_realCF from MinlosAnalytic.

theorem GFFIsGaussian.gff_slice_analytic_z0 (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (t : ℂ) : AnalyticOnNhd ℂ (fun (z₀ : ℂ) => GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (z₀ • toComplex f + t • toComplex g)) Set.univ

Key technical lemma: fixing one coordinate, the slice is analytic in the other. For z₀ ↦ Z[z₀•f + t•g] where t is a fixed complex number. Derived from OS0 by composition with linear embedding z₀ ↦ ![z₀, t].

theorem GFFIsGaussian.gff_slice_analytic_z1 (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (z₀ : ℂ) : AnalyticOnNhd ℂ (fun (z₁ : ℂ) => GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (z₀ • toComplex f + z₁ • toComplex g)) Set.univ

Derived from gff_slice_analytic_z0 by swapping f ↔ g and using add_comm.

theorem GFFIsGaussian.gaussian_rhs_slice_analytic_z0 (m : ℝ) (f g : TestFunction) (t : ℂ) : AnalyticOnNhd ℂ (fun (z₀ : ℂ) => Complex.exp (-(1 / 2) * (z₀ ^ 2 * ↑(QFT.freeCovarianceFormR m f f) + 2 * z₀ * t * ↑(QFT.freeCovarianceFormR m f g) + t ^ 2 * ↑(QFT.freeCovarianceFormR m g g)))) Set.univ

Slice of Gaussian RHS is analytic (exp of polynomial).

theorem GFFIsGaussian.gaussian_rhs_slice_analytic_z1 (m : ℝ) (f g : TestFunction) (z₀ : ℂ) : AnalyticOnNhd ℂ (fun (z₁ : ℂ) => Complex.exp (-(1 / 2) * (z₀ ^ 2 * ↑(QFT.freeCovarianceFormR m f f) + 2 * z₀ * z₁ * ↑(QFT.freeCovarianceFormR m f g) + z₁ ^ 2 * ↑(QFT.freeCovarianceFormR m g g)))) Set.univ

Slice of Gaussian RHS is analytic in the second variable.

theorem GFFIsGaussian.gff_cf_agrees_on_reals_OS0 (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (t s : ℝ) : GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (↑t • toComplex f + ↑s • toComplex g) = Complex.exp (-(1 / 2) * (↑t ^ 2 * ↑(QFT.freeCovarianceFormR m f f) + 2 * ↑t * ↑s * ↑(QFT.freeCovarianceFormR m f g) + ↑s ^ 2 * ↑(QFT.freeCovarianceFormR m g g)))

The GFF CF and Gaussian formula agree on ℝ². This follows from gff_cf_two_testfunctions by converting between types.

theorem GFFIsGaussian.gff_complex_characteristic_OS0 (m : ℝ) [Fact (0 < m)] (J : TestFunctionℂ) : GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) J = Complex.exp (-(1 / 2) * freeCovarianceℂBilinear m J J)

Complex generating functional for the free GFF via OS0 + identity theorem. This proves the result WITHOUT using twoD_line_from_realCF.

Polarization-Based Proof

The key insight is to use the polarization identity instead of derivative calculus.

For a centered Gaussian:

• E[⟨ω,f⟩²] = Q(f,f) (this is gff_second_moment_eq_covariance from GFFbridge)

By polarization:

• E[XY] = ¼(E[(X+Y)²] - E[(X-Y)²])
• With X = ⟨ω,f⟩, Y = ⟨ω,g⟩: E[⟨ω,f⟩⟨ω,g⟩] = ¼(Q(f+g,f+g) - Q(f-g,f-g)) = Q(f,g)

This avoids all derivative calculus!

theorem GFFIsGaussian.schwinger_eq_covariance_real (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : ∫ (ω : FieldConfiguration), ω f * ω g ∂↑(gaussianFreeFieldFree m) = QFT.freeCovarianceFormR m f g

For real test functions, the second moment equals the covariance. S₂(f,g) = Q(f,g) = freeCovarianceFormR(f,g)

Proof via polarization identity: E[XY] = ¼(E[(X+Y)²] - E[(X-Y)²]) = ¼(Q(f+g,f+g) - Q(f-g,f-g)) = Q(f,g) by bilinearity

theorem GFFIsGaussian.schwinger_eq_covarianceℂ_on_reals (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) (toComplex f) (toComplex g) = freeCovarianceℂBilinear m (toComplex f) (toComplex g)

For real test functions embedded into complex, the Schwinger 2-point function equals the complex covariance.

Main Theorems (at root level for compatibility)

theorem gff_two_point_equals_covarianceℂ_free (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f g = freeCovarianceℂBilinear m f g

For complex test functions, the Schwinger 2-point function equals the complex covariance.

S₂(μ, f, g) = freeCovarianceℂBilinear m f g

This extends schwinger_eq_covariance_real to complex test functions by bilinearity: both S₂ and freeCovarianceℂBilinear are bilinear, and they agree on real inputs.

For any complex f = fRe + I•fIm, g = gRe + I•gIm, we expand by bilinearity.

theorem gff_complex_generating (m : ℝ) [Fact (0 < m)] (J : TestFunctionℂ) : GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) J = Complex.exp (-(1 / 2) * SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) J J)

Complex generating functional for the free GFF: Z[J] = exp(-½ S₂(J,J))

This follows from gff_real_characteristic (for real J) extended to complex J via analyticity (gaussianFreeField_satisfies_OS0). Both sides are analytic in J and agree on real J, hence they are equal everywhere.

theorem isGaussianGJ_gaussianFreeField_free (m : ℝ) [Fact (0 < m)] : isGaussianGJ (gaussianFreeFieldFree m)

The Gaussian Free Field constructed via Minlos is Gaussian.

This combines:

1. Centering: E[⟨ω,φ⟩] = 0 (from gaussianFreeField_free_centered)
2. Gaussian CF: Z[J] = exp(-½ S₂(J,J)) (from gff_complex_generating)