Schwinger Two-Point Function

This file defines the two-point Schwinger function S₂(x) = ⟨φ(x)φ(0)⟩ as the limit of smeared correlations as the smearing functions approach Dirac deltas.

For mollifiers φ_ε (smooth, nonnegative, integral 1, support shrinking to 0): S₂(x) := lim_{ε→0} SchwingerFunction₂ dμ (φ_ε(·-x)) (φ_ε) = lim_{ε→0} ∫∫ φ_ε(u-x) ⟨φ(u)φ(v)⟩ φ_ε(v) du dv

For the GFF with covariance kernel C, this equals C(x) by double_mollifier_convergence.

Two-Point Schwinger Function Infrastructure

noncomputable def bumpToSchwartz (φ : ContDiffBump 0) : TestFunction

Convert a ContDiffBump centered at 0 to a normalized Schwartz function. This produces the L¹-normalized version φ.normed volume, which integrates to 1. Bump functions have compact support and are smooth, so they are Schwartz.

Equations

• bumpToSchwartz φ = ⋯.toSchwartzMap ⋯

@[simp]

theorem bumpToSchwartz_apply (φ : ContDiffBump 0) (x : SpaceTime) : (bumpToSchwartz φ) x = φ.normed MeasureTheory.volume x

bumpToSchwartz produces the L¹-normalized bump function.

noncomputable def translateSchwartz (f : TestFunction) (a : SpaceTime) : TestFunction

Translate a Schwartz function by a vector. This is an alias for SchwartzMap.translate specialized to SpaceTime.

Translation preserves smoothness and decay properties. See SchwartzMap.translate in FunctionalAnalysis.lean for the general version.

Equations

• translateSchwartz f a = SchwartzMap.translate f a

noncomputable def SmearedTwoPointFunction (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (φ : ContDiffBump 0) (x : SpaceTime) : ℝ

The smeared two-point function using a bump function. This is well-defined (modulo bumpToSchwartz) and converges to the pointwise value as the bump width → 0.

SmearedTwoPointFunction dμ φ x = ∫∫ φ(u-x) ⟨φ(u)φ(v)⟩ φ(v) du dv

Equations

• SmearedTwoPointFunction dμ_config φ x = SchwingerFunction₂ dμ_config (translateSchwartz (bumpToSchwartz φ) x) (bumpToSchwartz φ)

noncomputable def standardBumpSequence (n : ℕ) (hn : n ≠ 0) : ContDiffBump 0

A canonical sequence of bump functions with rOut → 0. We use rOut = 1/n for n ∈ ℕ⁺.

Equations

• standardBumpSequence n hn = { rIn := 1 / (2 * ↑n), rOut := 1 / ↑n, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

noncomputable def SchwingerTwoPointFunction (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (x : SpaceTime) : ℝ

Two-point correlation function defined as the limit of smeared correlations.

Definition: S₂(x) := lim_{n→∞} SmearedTwoPointFunction dμ (φ_{1/n}) x

where φ_ε is a standard bump function with outer radius ε.

This replaces the old DiracDelta-based definition, which was conceptually correct but used sorry since delta functions are distributions, not test functions.

Regularization at coincident points: At x = 0, the two-point function is mathematically undefined (it would be infinite for most QFTs). We regularize by setting S₂(0) = 0, which is consistent with the convention used in freeCovarianceKernel and makes the decay bounds hold trivially at x = 0.

For the GFF, this limit equals freeCovarianceKernel(x) by double_mollifier_convergence.

Equations

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

@[simp]

theorem schwingerTwoPointFunction_zero (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) : SchwingerTwoPointFunction dμ_config 0 = 0

SchwingerTwoPointFunction vanishes at coincident points by definition.

theorem smearedTwoPoint_tendsto_schwingerTwoPoint (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (x : SpaceTime) (hx : x ≠ 0) {ι : Type u_1} {l : Filter ι} [l.NeBot] (φ : ι → ContDiffBump 0) (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (C : SpaceTime → ℝ) (hC : ContinuousOn C {y : SpaceTime | y ≠ 0}) (hS₂ : ∀ (f g : TestFunction), SchwingerFunction₂ dμ_config f g = ∫ (u : SpaceTime) (v : SpaceTime), f u * C (u - v) * g v) : Filter.Tendsto (fun (i : ι) => SmearedTwoPointFunction dμ_config (φ i) x) l (nhds (C x))

The smeared two-point function converges to SchwingerTwoPointFunction as bump width → 0.

This justifies the limit-based definition of SchwingerTwoPointFunction. For measures with continuous covariance kernels (like the GFF), the limit exists and equals the kernel value.

Key hypothesis: We assume there exists a continuous (away from 0) kernel C such that SchwingerFunction₂ computes the double integral against C. This holds for Gaussian measures where C is the covariance kernel.

The proof uses double_mollifier_convergence from FunctionalAnalysis.lean.

theorem schwingerTwoPointFunction_eq_kernel (dμ_config : MeasureTheory.ProbabilityMeasure FieldConfiguration) (x : SpaceTime) (hx : x ≠ 0) (C : SpaceTime → ℝ) (hC : ContinuousOn C {y : SpaceTime | y ≠ 0}) (hS₂ : ∀ (f g : TestFunction), SchwingerFunction₂ dμ_config f g = ∫ (u : SpaceTime) (v : SpaceTime), f u * C (u - v) * g v) : SchwingerTwoPointFunction dμ_config x = C x

For measures with a continuous kernel C, the SchwingerTwoPointFunction equals C(x).

This is the key result: if the measure has an underlying continuous covariance kernel, then the limit-based definition of SchwingerTwoPointFunction evaluates to that kernel.

Note: For x = 0, the SchwingerTwoPointFunction is defined to be 0 by regularization, so this theorem requires x ≠ 0.