OS1 — Regularity (Exponential Bounds)

Proves |Z[f]| ≤ exp(c · ‖f‖²_{L²}) with p = 2 and c = 1/(2m²). The argument:

1. |Z[f]| = exp(−½ Re⟨f, Cf⟩_ℂ)
2. Decompose f = f_re + i·f_im, then Re⟨f, Cf⟩ = ⟨f_re, Cf_re⟩ − ⟨f_im, Cf_im⟩
3. Since C is positive semidefinite, −Re⟨f, Cf⟩ ≤ ⟨f_im, Cf_im⟩
4. In momentum space: ⟨g, Cg⟩ = ∫ |ĝ(k)|²/(|k|²+m²) dk ≤ ‖g‖²_{L²}/m² (Plancherel + bound 1/(|k|²+m²) ≤ 1/m²)
5. Combine: |Z[f]| ≤ exp(‖f‖²_{L²}/(2m²))

Local integrability of the two-point function C(x,0) ∼ 1/(4π²|x|²) follows from the Bessel K₁ asymptotics: (m/4π²|x|)K₁(m|x|) is locally integrable in 4D.

Main result

• gaussianFreeField_satisfies_OS1_revised

Preliminaries

theorem fourier_plancherel_schwartz (g : TestFunctionℂ) : ∫ (k : SpaceTime), ‖((SchwartzMap.fourierTransformCLM ℂ) g) k‖ ^ 2 = ∫ (x : SpaceTime), ‖g x‖ ^ 2

Plancherel (Schwartz): L² norm preservation for the Fourier transform. This follows directly from Mathlib's SchwartzMap.integral_norm_sq_fourier. Mathlib's Fourier transform is unitary-normalized, so no multiplicative constant is needed.

noncomputable def schwingerTwoPointFunctionGFF (m : ℝ) [hm : Fact (0 < m)] (x : SpaceTime) : ℝ

Two-point Schwinger function equals the free covariance kernel.

This is the fundamental connection between the abstract limit-based definition and the concrete position-space propagator.

Mathematically: ⟨φ(x)φ(0)⟩_μ = C(x, 0) for the Gaussian measure with covariance C.

Justification: This follows from the double mollifier convergence theorem. The two-point function S₂(x) is defined as the limit of smeared correlations: S₂(x) = lim_{ε→0} ∫∫ φ_ε(u-x) ⟨φ(u)φ(v)⟩ φ_ε(v) du dv = lim_{ε→0} (φ_ε ⋆ (φ_ε ⋆ C))(x) = C(x) for x ≠ 0

See double_mollifier_convergence in FunctionalAnalysis.lean for the general result.

Note: The abstract SchwingerTwoPointFunction in OS_Axioms.lean is now defined as a limit (using limUnder), properly avoiding DiracDelta. For the GFF specifically, we use this direct definition for computational convenience.

Equations

• schwingerTwoPointFunctionGFF m x = freeCovarianceKernel m x

theorem schwingerTwoPoint_eq_freeCovarianceKernel (m : ℝ) [Fact (0 < m)] (x : SpaceTime) : schwingerTwoPointFunctionGFF m x = freeCovarianceKernel m x

The GFF two-point function equals the free covariance kernel by definition.

theorem schwingerTwoPointFunction_eq_GFF (m : ℝ) [Fact (0 < m)] (x : SpaceTime) (hx : x ≠ 0) : SchwingerTwoPointFunction (gaussianFreeFieldFree m) x = schwingerTwoPointFunctionGFF m x

Compatibility: The abstract SchwingerTwoPointFunction agrees with the concrete definition for the GFF. This uses the limit-based definition of SchwingerTwoPointFunction and the double mollifier convergence theorem via schwingerTwoPointFunction_eq_kernel.

The proof requires:

1. Continuity of freeCovarianceKernel away from 0
2. SchwingerFunction₂ for the GFF computes ∫∫ f(u) C(u-v) g(v) du dv

Both are standard properties of the GFF; the sorries encode these standard facts.

theorem schwingerTwoPointFunction_eq_freeCovarianceKernel (m : ℝ) [Fact (0 < m)] (x : SpaceTime) (hx : x ≠ 0) : SchwingerTwoPointFunction (gaussianFreeFieldFree m) x = freeCovarianceKernel m x

The abstract SchwingerTwoPointFunction equals freeCovarianceKernel for the GFF. This is the version needed for downstream proofs using TwoPointIntegrable. Note: Only holds for x ≠ 0 since the covariance is undefined at coincident points.

theorem schwinger_two_point_decay_bound_GFF (m : ℝ) [Fact (0 < m)] : ∃ C > 0, ∀ (x y : SpaceTime), ‖schwingerTwoPointFunctionGFF m (x - y)‖ ≤ C * ‖x - y‖ ^ (-2)

The GFF two-point Schwinger function satisfies a polynomial decay bound. For the free field, this follows from the Bessel function asymptotics:

• Near origin: K₁(mr) ~ 1/(mr), giving decay like 1/r²
• Far from origin: K₁(mr) ~ exp(-mr), which is even faster decay

theorem schwinger_two_point_decay_bound (m : ℝ) [Fact (0 < m)] : ∃ C > 0, ∀ (x y : SpaceTime), ‖SchwingerTwoPointFunction (gaussianFreeFieldFree m) (x - y)‖ ≤ C * ‖x - y‖ ^ (-2)

The abstract two-point Schwinger function satisfies a polynomial decay bound. Uses the bridge lemma to connect to the concrete GFF definition. Note: At x = y (coincident points), the bound still holds since the abstract definition regularizes S(0) = 0 and 0^(-2) = 0 by Mathlib convention.

theorem schwingerTwoPoint_measurable (m : ℝ) [Fact (0 < m)] : MeasureTheory.AEStronglyMeasurable (fun (x : SpaceTime) => SchwingerTwoPointFunction (gaussianFreeFieldFree m) x) MeasureTheory.volume

The abstract two-point Schwinger function is measurable. This uses the bridge lemma to connect to the concrete GFF definition. The functions agree on the complement of {0}, which has full measure.

GFF Exponential Bound

Elementary bound on the GFF generating function using complex exponential properties.

theorem gff_generating_norm_eq (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : ‖GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) f‖ = Real.exp (-(1 / 2) * (freeCovarianceℂBilinear m f f).re)

The norm of the GFF generating function equals the exponential of minus one-half the real part of the covariance. This is an elementary property of complex exponentials: |exp(z)| = exp(Re z).

theorem gff_generating_bound_by_imaginary (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : Real.exp (-(1 / 2) * (freeCovarianceℂBilinear m f f).re) ≤ Real.exp (1 / 2 * (freeCovarianceℂBilinear m (toComplex (complexTestFunctionDecompose f).2) (toComplex (complexTestFunctionDecompose f).2)).re)

Using bilinearity and the real/imaginary decomposition, the real part of C(f,f) satisfies Re C(f,f) = C(Re f, Re f) - C(Im f, Im f). Combined with monotonicity of exp, this gives the bound exp(-1/2 Re C(f,f)) ≤ exp(1/2 C(Im f, Im f)).

theorem covariance_imaginary_L2_bound (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : (freeCovarianceℂBilinear m (toComplex (complexTestFunctionDecompose f).2) (toComplex (complexTestFunctionDecompose f).2)).re ≤ 1 / m ^ 2 * ∫ (x : SpaceTime), ‖f x‖ ^ 2

theorem gff_generating_L2_bound (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : ‖GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) f‖ ≤ Real.exp (1 / (2 * m ^ 2) * ∫ (x : SpaceTime), ‖f x‖ ^ 2)

The GFF generating functional satisfies the exponential bound |Z[f]| ≤ exp((1/2m²)||f||²_{L²}). This combines the norm equality, the bound by imaginary part, and the L² bound to give the final OS1 estimate.

Two-Point Function Local Integrability

Using the axioms above, we establish local integrability of the Schwinger function.

theorem gff_two_point_locally_integrable (m : ℝ) [Fact (0 < m)] : TwoPointIntegrable (gaussianFreeFieldFree m)

The two-point Schwinger function is locally integrable. This follows from the polynomial decay bound |S_2(x)| ≤ C|x|^{-2}. In d=4 spacetime dimensions, |x|^{-2} is locally integrable since 2 < 4.

OS1 Verification for the GFF

Using the exponential L²-bound for the generating functional and local integrability of the two-point function, we verify OS1 as stated in OS_Axioms.lean (with the p-th power appearing inside the exponential).

theorem gaussianFreeField_satisfies_OS1_revised (m : ℝ) [Fact (0 < m)] : os1Regularity (gaussianFreeFieldFree m)

The Gaussian free field satisfies OS1 regularity with p = 2 and c = 1/(2 m^2). This uses gff_generating_L2_bound and gff_two_point_locally_integrable established above.

Note: Named _revised because the alternative OS0 proof in GaussianFreeField.lean uses the same module; both are valid, and OS.Master uses this one.