OS4 — Polynomial Clustering

Proves |𝔼[e^{⟨ω,f⟩+⟨T_s ω,g⟩}] − 𝔼[e^{⟨ω,f⟩}]·𝔼[e^{⟨ω,g⟩}]| ≤ c·(1+s)^{−α} for any α > 0.

The proof follows Steps 1–6 of §4.4.5:

1. Time-translation duality: ⟨T_s ω, g⟩ = ⟨ω, T_{−s}g⟩
2. Gaussian factorization: 𝔼[e^{⟨ω,f+T_{−s}g⟩}] = E_f · E_g · exp(S₂(f, T_{−s}g))
3. Subtract and bound: |…| ≤ |E_f|·|E_g|·|S₂(f,T_{−s}g)|·exp(|S₂(f,T_{−s}g)|)
4. S₂(f,T_{−s}g) = ∫∫ f(x) K(x−y) g(y−τ_s) dy dx with K = free covariance kernel
5. Quantitative decay: |∫∫ f(x) K(x−y) g(y−a) dy dx| ≤ c·(1+‖a‖)^{−α} via the convolution decay lemma (domain split at ‖y‖ = ‖x‖/2) applied to the exponentially decaying kernel |K(z)| ≤ C·e^{−m‖z‖}
6. Combine with |e^z−1| ≤ |z|·e^{|z|} to close.

Main result

• gaussianFreeField_satisfies_OS4

Gaussian Generating Functional Factorization

theorem QFT.schwinger2_sum_expansion (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) (f + g) (f + g) = SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f f + 2 * SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f g + SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) g g

Bilinearity expansion of the Schwinger 2-point function for sums.

S₂(f+g, f+g) = S₂(f,f) + S₂(f,g) + S₂(g,f) + S₂(g,g) = S₂(f,f) + 2·S₂(f,g) + S₂(g,g) (by symmetry)

This uses the bilinearity proved in Measure.IsGaussian.

theorem QFT.gff_generating_sum_factorization (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (f + g) = GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) f * GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) g * Complex.exp (-SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f g)

For Gaussian measures, the generating functional of a sum factorizes up to a cross term: Z[f + g] = Z[f] · Z[g] · exp(-⟨f, Cg⟩)

This follows from expanding ⟨f+g, C(f+g)⟩ = ⟨f,Cf⟩ + 2⟨f,Cg⟩ + ⟨g,Cg⟩.

Compare with gaussianFreeField_real_entry_factor in OS.os3ReflectionPositivity which proves the analogous factorization for real test functions.

Cross Covariance Decay

Translation as Euclidean Action

theorem QFT.LinearIsometry_inv_one : LinearIsometry.inv 1 = 1

The inverse of the identity linear isometry is itself.

Translation Invariance from OS2

theorem QFT.generating_euclidean_invariant (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (h_inv : os2EuclideanInvariance dμ_config) (g : E) (f : TestFunctionℂ) : GJGeneratingFunctionalℂ dμ_config (euclideanAction g f) = GJGeneratingFunctionalℂ dμ_config f

For OS2-invariant measures, Z[euclideanAction g f] = Z[f] for any g ∈ E.

GFF Generating Functional Norm Bound

theorem QFT.gff_generating_norm_le_one_real (m : ℝ) [Fact (0 < m)] (f : TestFunction) : ‖GJGeneratingFunctionalℂ (gaussianFreeFieldFree m) (toComplex f)‖ ≤ 1

The GFF generating functional has norm at most 1 for real test functions.

For Gaussian measures with positive definite covariance C and real test function f: Z[f] = exp(-½⟨f, Cf⟩)

Since the covariance is positive definite on real functions (⟨f, Cf⟩ ≥ 0), we have |Z[f]| = exp(-½⟨f, Cf⟩) ≤ exp(0) = 1.

NOTE: For complex test functions f = fRe + i*fIm, the bilinear form satisfies Re C_bilin(f,f) = C(fRe,fRe) - C(fIm,fIm), which can be negative! The bound |Z[f]| ≤ 1 does NOT hold for general complex f. Instead, use gff_generating_L2_bound from OS.os1Regularity for the general case.

Technical Lemma for OS4 (Real Test Functions)

theorem QFT.GFF_OS4_from_small_decay_real (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (a : SpaceTime) (δ : ℝ) (_hδ_pos : δ > 0) (hδ_small : δ ≤ 1) (h_decay : ‖SchwingerFunction₂ (gaussianFreeFieldFree m) f (SchwartzMap.translate g a)‖ < δ) : ‖GJGeneratingFunctional (gaussianFreeFieldFree m) (f + SchwartzMap.translate g a) - GJGeneratingFunctional (gaussianFreeFieldFree m) f * GJGeneratingFunctional (gaussianFreeFieldFree m) g‖ < 2 * δ

Technical lemma: OS4 bound from cross-term decay for real test functions.

Given that |S₂(f, T_a g)| < δ with δ ≤ 1, conclude |Z[f + T_a g] - Z[f]·Z[g]| < 2δ.

Uses:

• Factorization: Z[f + T_a g] = Z[f]·Z[T_a g]·exp(-S₂(f, T_a g))
• Translation invariance: Z[T_a g] = Z[g] (from OS2)
• Combined: Z[f + T_a g] = Z[f]·Z[g]·exp(-S₂(f, T_a g))
• Therefore: Z[f + T_a g] - Z[f]·Z[g] = Z[f]·Z[g]·(exp(-S₂(f, T_a g)) - 1)
• Real test function bound: |Z[f]| ≤ 1 for real f (positive definite covariance)
• Exponential estimate: |exp(-z) - 1| ≤ 2|z| for |z| ≤ 1

Main Theorem: OS4 for Gaussian Free Field

theorem QFT.schwartz_cross_covariance_decay_real (m : ℝ) [Fact (0 < m)] (f g : TestFunction) (ε : ℝ) (hε : ε > 0) : ∃ R > 0, ∀ (a : SpaceTime), ‖a‖ > R → ‖SchwingerFunction₂ (gaussianFreeFieldFree m) f (SchwartzMap.translate g a)‖ < ε

Cross covariance decay for real Schwartz functions.

The 2-point function S₂(f, T_a g) → 0 as |a| → ∞ for Schwartz functions. This follows from:

• The kernel C(z) decays like 1/|z|² at large distances (freeCovarianceKernel_decay_bound)
• Schwartz functions are L¹ integrable
• schwartz_bilinear_translation_decay

Uses the covariance representation: S₂(f, T_a g) = ∫∫ f(x) · C(x-y) · g(y-a) dx dy

theorem QFT.gaussianFreeField_satisfies_OS4 (m : ℝ) [Fact (0 < m)] : os4Clustering (gaussianFreeFieldFree m)

The Gaussian Free Field satisfies OS4 clustering.

The proof combines:

1. Gaussian factorization: Z[f + T_a g] = Z[f] · Z[T_a g] · exp(-S₂(f, T_a g))
2. Translation invariance: Z[T_a g] = Z[g] (from OS2)
3. Cross term decay: S₂(f, T_a g) → 0 as |a| → ∞
4. Continuity: exp(-z) → exp(0) = 1 as z → 0
5. For real test functions: |Z[f]| ≤ 1 (positive definite covariance)

Alternative: Direct (ε-δ) Formulation

These are not used in the main OS4 proof path (which goes through os4PolynomialClustering), but kept as an alternative qualitative formulation of clustering.

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

Covariance clustering property: the 2-point function decays at large separations.

Equations

• QFT.covarianceClusteringReal dμ_config = ∀ (f g : TestFunction), ∀ ε > 0, ∃ R > 0, ∀ (a : SpaceTime), ‖a‖ > R → ‖SchwingerFunction₂ dμ_config f (SchwartzMap.translate g a)‖ < ε

theorem QFT.freeCovarianceClustering_real (m : ℝ) [Fact (0 < m)] : covarianceClusteringReal (gaussianFreeFieldFree m)

The free covariance has the clustering property.

OS4 Polynomial Clustering for GFF

The GFF satisfies polynomial clustering with any decay rate α > 0, because the underlying covariance has exponential decay (from the mass gap).

The proof uses:

1. Time translation duality: ⟨T_s ω, g⟩ = ⟨ω, T_{-s} g⟩
2. Gaussian factorization: E[e^{⟨ω, f + T_{-s} g⟩}] = Z[f]·Z[g]·exp(-S₂(f, T_{-s} g))
3. The proved theorem schwartz_bilinear_translation_decay_polynomial_proof for polynomial bounds

Time Translation Infrastructure for Polynomial Clustering

For os4PolynomialClustering, we need to work with time translation of distributions. The key duality is: ⟨T_s ω, g⟩ = ⟨ω, T_{-s} g⟩

This connects time translation of distributions to translation of test functions.

noncomputable def QFT.timeVector (s : ℝ) : SpaceTime

Time translation vector: shifts only the time coordinate by s. timeVector s = (s, 0, 0, 0) in coordinates.

Equations

• QFT.timeVector s = (EuclideanSpace.equiv (Fin STDimension) ℝ).symm fun (i : Fin STDimension) => if i = 0 then s else 0

theorem QFT.time_translation_pairing_duality (s : ℝ) (ω : FieldConfiguration) (g : TestFunctionℂ) : distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) g = distributionPairingℂReal ω (TimeTranslation.timeTranslationSchwartzℂ (-s) g)

Time duality for distribution pairing: ⟨T_s ω, g⟩ = ⟨ω, T_{-s} g⟩. This is the fundamental identity connecting time translation of distributions to time translation of test functions.

Note: This uses the definition of timeTranslationDistribution from TimeTranslation.lean, which is defined by duality: (T_s ω)(f) = ω(T_{-s} f).

The proof follows from:

1. timeTranslationDistribution_apply: (T_s ω)(f) = ω(T_{-s} f) for real test functions
2. Time translation commutes with taking real/imaginary parts of complex Schwartz functions

Key Lemmas for Connecting Bilinear Decay to Schwinger Function

theorem QFT.timeShiftConst_norm (s : ℝ) : ‖TimeTranslation.timeShiftConst s‖ = |s|

The time shift constant vector (s, 0, 0, 0) has norm |s|.

theorem QFT.timeTranslationSchwartzℂ_at_point (s : ℝ) (g : TestFunctionℂ) (y : SpaceTime) : (TimeTranslation.timeTranslationSchwartzℂ s g) y = g (TimeTranslation.timeShift s y)

Time translation of Schwartz function at a point equals function evaluated at shifted point.

theorem QFT.timeShift_eq_add (s : ℝ) (y : SpaceTime) : TimeTranslation.timeShift s y = y + TimeTranslation.timeShiftConst s

Time shift by s equals adding the time shift constant.

theorem QFT.timeTranslationSchwartzℂ_neg_eq_sub (s : ℝ) (g : TestFunctionℂ) (y : SpaceTime) : (TimeTranslation.timeTranslationSchwartzℂ (-s) g) y = g (y - TimeTranslation.timeShiftConst s)

Time translation by -s gives g(y - timeShiftConst(s)).

theorem QFT.freeCovariance_eq_kernel (m : ℝ) (x y : SpaceTime) : freeCovariance m x y = freeCovarianceKernel m (x - y)

freeCovariance is translation-invariant: C(x,y) = C(0, x-y) = freeCovarianceKernel(x-y).

theorem QFT.schwinger2_time_translated_eq_bilinear (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) (s : ℝ) : SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f (TimeTranslation.timeTranslationSchwartzℂ (-s) g) = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovarianceKernel m (x - y)) * g (y - TimeTranslation.timeShiftConst s)

The Schwinger 2-point function for time-translated test function equals the bilinear integral with translated argument.

theorem QFT.gaussianFreeField_satisfies_OS4_PolynomialClustering (m : ℝ) [Fact (0 < m)] (α : ℝ) (hα : α > 0) : os4PolynomialClustering (gaussianFreeFieldFree m) α hα

The GFF satisfies OS4 polynomial clustering for any exponent α > 0.

The proof uses:

1. Time duality: ⟨T_s ω, g⟩ = ⟨ω, T_{-s} g⟩
2. Gaussian factorization: E[e^{⟨ω, f⟩ + ⟨T_s ω, g⟩}] = Z[f]·Z[g]·exp(-S₂(f, T_{-s} g))
3. Exponential covariance decay: |S₂(f, T_{-s} g)| ≤ c·e^{-ms} from mass gap
4. Proved theorem: schwartz_bilinear_translation_decay_polynomial_proof for polynomial bound

The mass gap m > 0 ensures exponential decay, which is stronger than any polynomial. Therefore the GFF satisfies os4PolynomialClustering for all α > 0.