OS4 — Shared Infrastructure

Shared lemmas for os4Clustering and OS4Ergodicity:

• Time translation duality: ⟨T_s ω, g⟩ = ⟨ω, T_{−s} g⟩
• GFF MGF formula: 𝔼[e^{⟨ω,f⟩}] = exp(½ S₂(f,f)) and its time-translation invariance
• Joint MGF factorization: 𝔼[e^{⟨ω,f+T_{−s}g⟩}] = E_f · E_g · exp(S₂(f, T_{−s}g))
• Exponential bound: |e^z − 1| ≤ |z| · e^{|z|}

Time Translation Infrastructure

We re-export the core TimeTranslation API so that importers of OS4infra get these names in scope without a separate TimeTranslation import.

Time Translation Decomposition Lemmas

theorem OS4infra.timeTranslationSchwartzℂ_decompose_fst (s : ℝ) (g : TestFunctionℂ) : (complexTestFunctionDecompose (timeTranslationSchwartzℂ s g)).1 = timeTranslationSchwartz s (complexTestFunctionDecompose g).1

Time translation commutes with real part extraction for complex Schwartz functions.

theorem OS4infra.timeTranslationSchwartzℂ_decompose_snd (s : ℝ) (g : TestFunctionℂ) : (complexTestFunctionDecompose (timeTranslationSchwartzℂ s g)).2 = timeTranslationSchwartz s (complexTestFunctionDecompose g).2

Time translation commutes with imaginary part extraction for complex Schwartz functions.

theorem OS4infra.timeTranslationDistribution_pairingℂ (s : ℝ) (ω : FieldConfiguration) (g : TestFunctionℂ) : distributionPairingℂReal (timeTranslationDistribution s ω) g = distributionPairingℂReal ω (timeTranslationSchwartzℂ (-s) g)

Time translation on distributions is compatible with complex pairing. ⟨T_s ω, g⟩ℂ = ⟨ω, T{-s} g⟩_ℂ

Continuity of Complex Pairing under Time Translation

theorem OS4infra.continuous_distributionPairingℂ_timeTranslation (ω : FieldConfiguration) (g : TestFunctionℂ) : Continuous fun (s : ℝ) => distributionPairingℂReal (timeTranslationDistribution s ω) g

s ↦ ⟨T_s ω, g⟩_ℂ is continuous. Uses the proved continuous_timeTranslationSchwartz.

Euclidean Group Infrastructure for Time Translation

noncomputable def OS4infra.timeTranslationE (t : ℝ) : QFT.E

Time translation as a Euclidean group element. timeTranslationE t = (1, -timeShiftConst t) where 1 is the identity rotation.

Equations

• OS4infra.timeTranslationE t = { R := 1, t := -TimeTranslation.timeShiftConst t }

theorem OS4infra.euclidean_action_timeTranslationE (t : ℝ) (f : TestFunctionℂ) : QFT.euclideanAction (timeTranslationE t) f = timeTranslationSchwartzℂ t f

The Euclidean action of timeTranslationE equals timeTranslationSchwartzℂ.

GFF Covariance Invariance

theorem OS4infra.freeCovarianceℂ_bilinear_timeTranslation_invariant (m : ℝ) [Fact (0 < m)] (t : ℝ) (f g : TestFunctionℂ) : freeCovarianceℂBilinear m (timeTranslationSchwartzℂ t f) (timeTranslationSchwartzℂ t g) = freeCovarianceℂBilinear m f g

The GFF covariance is invariant under simultaneous time translation.

GFF Moment Generating Function

theorem OS4infra.gff_mgf_formula (m : ℝ) [Fact (0 < m)] (J : TestFunctionℂ) : ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω J) ∂↑(gaussianFreeFieldFree m) = Complex.exp (1 / 2 * freeCovarianceℂBilinear m J J)

MGF formula for GFF: ∫ exp(⟨ω,J⟩) dμ = exp(+(1/2) * C(J,J)). This follows from the characteristic function formula via substitution J → (-I)•J.

theorem OS4infra.gff_generating_time_invariant (m : ℝ) [Fact (0 < m)] (s : ℝ) (f : TestFunctionℂ) : ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω (timeTranslationSchwartzℂ s f)) ∂↑(gaussianFreeFieldFree m) = ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂↑(gaussianFreeFieldFree m)

The GFF generating function is invariant under time translation.

Joint MGF Factorization

theorem OS4infra.gff_joint_mgf_factorization (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f + distributionPairingℂReal ω g) ∂↑(gaussianFreeFieldFree m) = ((∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω f) ∂↑(gaussianFreeFieldFree m)) * ∫ (ω : FieldConfiguration), Complex.exp (distributionPairingℂReal ω g) ∂↑(gaussianFreeFieldFree m)) * Complex.exp (SchwingerFunctionℂ₂ (gaussianFreeFieldFree m) f g)

Joint MGF factorization for GFF. E[e^{⟨ω,f⟩+⟨ω,g⟩}] = E[e^{⟨ω,f⟩}] E[e^{⟨ω,g⟩}] e^{C(f,g)} This follows from the GFF being Gaussian.

Exponential Bound

theorem OS4infra.exp_sub_one_bound_general (x : ℂ) : ‖Complex.exp x - 1‖ ≤ ‖x‖ * Real.exp ‖x‖

‖e^x - 1‖ ≤ ‖x‖ · e^{‖x‖} for complex x.