OS4 — Ergodicity from Polynomial Clustering

Proves (1/t)∫₀ᵗ A(T_s φ) ds → 𝔼[A] in L²(μ) as t → ∞. The reduction chain:

1. Minkowski inequality reduces from A = ∑ cⱼ e^{⟨φ,fⱼ⟩} to single exponentials
2. L² variance bound (Fubini + Fernique): ‖(1/t)∫₀ᵗ e^{⟨T_s φ,f⟩} ds − 𝔼[e^{⟨φ,f⟩}]‖²_{L²} = (1/t²) ∫₀ᵗ∫₀ᵗ 𝔼[(…)(…)] ds ds'
3. Polynomial clustering gives |𝔼[…]| ≤ c·(1+|s−s'|)^{−2}
4. Final bound: ≤ (c/t) ∫_{−∞}^{∞} (1+|s|)^{−2} ds → 0

Uses α = 6 from the spatial dimension d = 3 (mass gap).

Main result

• OS4_PolynomialClustering_implies_OS4_Ergodicity

OS4 Axiom Variants

We define intermediate formulations of OS4 that are easier to prove directly.

def OS4Ergodicity.os4PrimeErgodicityGenerating (m : ℝ) [Fact (0 < m)] : Prop

OS4' (Ergodicity on generating functions): For any f ∈ S(ℝ × ℝ³), lim_{t→∞} (1/t) ∫₀ᵗ e^{⟨T_s φ, f⟩} ds → 𝔼_μ[e^{⟨φ,f⟩}] in L²(muGFF)

Equations

• One or more equations did not get rendered due to their size.

def OS4Ergodicity.os4DoublePrimeClustering (m : ℝ) [Fact (0 < m)] : Prop

OS4'' (Polynomial Clustering): This is exactly os4PolynomialClustering specialized to the GFF with decay exponent α = 6.

Equations

• OS4Ergodicity.os4DoublePrimeClustering m = os4PolynomialClustering (gaussianFreeFieldFree m) 6 OS4Ergodicity.os4DoublePrimeClustering._proof_2

GFF Integrability Lemmas

theorem OS4Ergodicity.gff_exp_pairing_integrable (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal ω f)) ↑(gaussianFreeFieldFree m)

The GFF exponential is integrable with respect to the GFF measure.

theorem OS4Ergodicity.gff_exp_time_translated_memLp_two (m : ℝ) [Fact (0 < m)] (s : ℝ) (f : TestFunctionℂ) : MeasureTheory.MemLp (fun (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f)) 2 ↑(gaussianFreeFieldFree m)

Time-translated complex exponential is in L² under the GFF measure. This follows from |exp(z)|² = exp(2 Re z) ≤ exp(2|Re z|) which is integrable. (Copied from OS4Ron.lean - needed for integrability proofs)

GFF Time Translation Invariance

theorem OS4Ergodicity.timeTranslationSchwartzℂ_conj_comm (t : ℝ) (f : TestFunctionℂ) : TimeTranslation.timeTranslationSchwartzℂ t (conjSchwartz f) = conjSchwartz (TimeTranslation.timeTranslationSchwartzℂ t f)

Time translation commutes with pointwise conjugation.

theorem OS4Ergodicity.gff_exp_product_time_shift_invariant (m : ℝ) [Fact (0 < m)] (g₁ g₂ : TestFunctionℂ) (t : ℝ) : have μ := ↑(gaussianFreeFieldFree m); ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω (TimeTranslation.timeTranslationSchwartzℂ t g₁)) * (starRingEnd ℂ) (Complex.exp (distributionPairingℂReal ω (TimeTranslation.timeTranslationSchwartzℂ t g₂))) ∂μ = ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω g₁) * (starRingEnd ℂ) (Complex.exp (distributionPairingℂReal ω g₂)) ∂μ

The product exp(⟨ω, T_t g₁⟩) · conj(exp(⟨ω, T_t g₂⟩)) integral is time-shift invariant. This follows from the GFF characteristic function and covariance time-translation invariance.

theorem OS4Ergodicity.gff_exp_L2_norm_constant (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (s : ℝ) : ∫ (ω : FieldConfiguration), ‖Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f)‖ ^ 2 ∂↑(gaussianFreeFieldFree m) = ∫ (ω : FieldConfiguration), ‖Complex.exp (distributionPairingℂReal ω f)‖ ^ 2 ∂↑(gaussianFreeFieldFree m)

The L² norm of A_s is constant in s by stationarity. Proof: Uses OS2 → gff_exp_product_time_shift_invariant → this result.

theorem OS4Ergodicity.time_average_memLp_two (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (T : ℝ) (hT : T > 0) : MeasureTheory.MemLp (fun (ω : FieldConfiguration) => 1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f)) 2 ↑(gaussianFreeFieldFree m)

The time average (1/T)∫A_s ds is in L²(μ).

theorem OS4Ergodicity.gff_err_sq_integrable (m : ℝ) [Fact (0 < m)] (T : ℝ) (hT : T > 0) (f : TestFunctionℂ) : MeasureTheory.Integrable (fun (ω : FieldConfiguration) => ‖((1 / T) • ∫ (s : ℝ) in Set.Icc 0 T, Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f)) - ∫ (ω' : FieldConfiguration), Complex.exp (distributionPairingℂReal ω' f) ∂↑(gaussianFreeFieldFree m)‖ ^ 2) ↑(gaussianFreeFieldFree m)

The error term squared is integrable (for T > 0).

Decay Integral Bounds

theorem OS4Ergodicity.double_integral_decay_bound : ∃ C > 0, ∀ T > 0, ∫ (s : ℝ) (u : ℝ) in Set.Icc 0 T, (1 + |s - u|) ^ (-3) ≤ 2 * T * C

Double integral bound: ∫∫_{[0,T]²} (1+|s-u|)^{-3} ≤ 2T·C for some constant C.

theorem OS4Ergodicity.gff_product_expectation_stationarity (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (s u : ℝ) : have μ := ↑(gaussianFreeFieldFree m); have A := fun (t : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution t ω) f); ∫ (ω : FieldConfiguration), A s ω * (starRingEnd ℂ) (A u ω) ∂μ = ∫ (ω : FieldConfiguration), A (s - u) ω * (starRingEnd ℂ) (A 0 ω) ∂μ

Product expectation stationarity.

GFF Covariance Continuity

theorem OS4Ergodicity.gff_covariance_timeTranslation_continuous (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : Continuous fun (s : ℝ) => SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) (TimeTranslation.timeTranslationSchwartzℂ s f) g

The Schwinger two-point function (covariance) is continuous under time translation. s ↦ C(T_s f, g) is continuous. (Proved via dominated convergence, copied from GFFCovarianceContinuity.)

theorem OS4Ergodicity.gff_covariance_continuous (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : have μ := ↑(gaussianFreeFieldFree m); have A := fun (t : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution t ω) f); have EA := ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂μ; Continuous fun (p : ℝ × ℝ) => ∫ (ω : FieldConfiguration), A p.1 ω * (starRingEnd ℂ) (A p.2 ω) ∂μ - EA * (starRingEnd ℂ) EA

The GFF covariance function (s, u) ↦ E[A_s · conj(A_u)] - E[A]·conj(E[A]) is continuous.

Proved using the Gaussian algebraic structure:

1. By stationarity, Cov(s,u) = g(s-u) for g(t) = E[A_t·conj(A_0)] - EA·conj(EA)
2. By Gaussian MGF formula, g(t) = EA·conj(EA)·(exp(C(T_{-t}f, conj(f))) - 1)
3. C(T_s f, g) is continuous in s by dominated convergence
4. Compose with exp and subtraction

Variance Bounds

theorem OS4Ergodicity.L2_time_average_variance_bound (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (T : ℝ) (hT : T > 0) : have μ := ↑(gaussianFreeFieldFree m); have A := fun (s : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f); have EA := ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂μ; have Cov := fun (s u : ℝ) => ∫ (ω : FieldConfiguration), A s ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA; ∫ (ω : FieldConfiguration), ‖(1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, A s ω) - EA‖ ^ 2 ∂μ ≤ 1 / T ^ 2 * ∫ (s : ℝ) (u : ℝ) in Set.Icc 0 T, ‖Cov s u‖

L² variance can be bounded by double integral of covariance.

This combines the integral bound (which gives ‖∫∫ Cov‖) with triangle inequality to get the bound in terms of ∫∫ ‖Cov‖ which is what we need for decay estimates.

Clustering Implies Covariance Decay

theorem OS4Ergodicity.clustering_implies_covariance_decay (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (h_cluster : os4DoublePrimeClustering m) : ∃ c ≥ 0, ∀ (s u : ℝ), s ≥ 0 → u ≥ 0 → have μ := ↑(gaussianFreeFieldFree m); have A := fun (t : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution t ω) f); have EA := ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂μ; ‖∫ (ω : FieldConfiguration), A s ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA‖ ≤ c * (1 + |s - u|) ^ (-3)

OS4'' clustering implies covariance decay with exponent -3.

theorem OS4Ergodicity.gff_covariance_norm_integrableOn_slice (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (s T : ℝ) : have μ := ↑(gaussianFreeFieldFree m); have A := fun (t : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution t ω) f); have EA := ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂μ; have Cov := fun (s' u : ℝ) => ∫ (ω : FieldConfiguration), A s' ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA; MeasureTheory.IntegrableOn (fun (u : ℝ) => ‖Cov s u‖) (Set.Icc 0 T) MeasureTheory.volume

The norm of the GFF covariance is integrable on [0,T] for each fixed first argument. Uses gff_covariance_norm_integrableOn_slice_axiom to avoid expensive type unification.

Variance Decay from Clustering

theorem OS4Ergodicity.variance_decay_from_clustering (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) (c : ℝ) (hc : c ≥ 0) (h_cov_decay : ∀ (s u : ℝ), s ≥ 0 → u ≥ 0 → have μ := ↑(gaussianFreeFieldFree m); have A := fun (t : ℝ) (ω : FieldConfiguration) => Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution t ω) f); have EA := ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂μ; ‖∫ (ω : FieldConfiguration), A s ω * (starRingEnd ℂ) (A u ω) ∂μ - EA * (starRingEnd ℂ) EA‖ ≤ c * (1 + |s - u|) ^ (-3)) : have μ := ↑(gaussianFreeFieldFree m); Filter.Tendsto (fun (T : ℝ) => ∫ (ω : FieldConfiguration), ‖1 / ↑T * ∫ (s : ℝ) in Set.Icc 0 T, Complex.exp (distributionPairingℂReal (TimeTranslation.timeTranslationDistribution s ω) f) - ∫ (ω' : FieldConfiguration), Complex.exp (distributionPairingℂReal ω' f) ∂μ‖ ^ 2 ∂μ) Filter.atTop (nhds 0)

Covariance decay implies variance tends to zero.

Main Theorem Chain

theorem OS4Ergodicity.norm_sq_weighted_sum_le {n : ℕ} (w a : Fin n → ℂ) : ‖∑ j : Fin n, w j * a j‖ ^ 2 ≤ (∑ j : Fin n, ‖w j‖ ^ 2) * ∑ j : Fin n, ‖a j‖ ^ 2

Bound for norm squared of weighted sum using Cauchy-Schwarz.

theorem OS4Ergodicity.OS4'_implies_OS4 (m : ℝ) [Fact (0 < m)] : os4PrimeErgodicityGenerating m → OS4Ergodicity (gaussianFreeFieldFree m)

OS4' → OS4: Generating function ergodicity implies full ergodicity.

The proof uses Cauchy-Schwarz to bound the variance of ∑ⱼ zⱼ exp(⟨ω, fⱼ⟩) by the sum of individual variances, then applies OS4' to each term.

theorem OS4Ergodicity.OS4''_implies_OS4' (m : ℝ) [Fact (0 < m)] : os4DoublePrimeClustering m → os4PrimeErgodicityGenerating m

OS4'' → OS4': Polynomial clustering implies generating function ergodicity.

theorem OS4Ergodicity.OS4''_implies_OS4_Ergodicity (m : ℝ) [Fact (0 < m)] : os4DoublePrimeClustering m → OS4Ergodicity (gaussianFreeFieldFree m)

OS4'' → OS4: The full chain from clustering to ergodicity.

theorem OS4Ergodicity.OS4_PolynomialClustering_implies_OS4_Ergodicity (m : ℝ) [Fact (0 < m)] : os4PolynomialClustering (gaussianFreeFieldFree m) 6 ⋯ → OS4Ergodicity (gaussianFreeFieldFree m)

Main Theorem: os4PolynomialClustering with α=6 implies OS4Ergodicity for the GFF.

This is the main result connecting the clustering axiom to ergodicity.