Momentum Space Propagator for Gaussian Free Field

This file implements the momentum space free propagator 1/(‖k‖²+m²) and its properties. This is the foundation for the free covariance function in position space, which is computed via Fourier transform.

Main Definitions

• freePropagatorMomentum: Momentum space propagator 1/(‖k‖²+m²)
• freeCovariance: Position space covariance via Fourier transform
• freeCovarianceKernel: Alternative name for compatibility
• propagatorMultiplication: Linear operator for multiplication by propagator

Key Results

• freePropagator_even: Propagator is an even function
• freeCovariance_symmetric: Covariance is symmetric C(x,y) = C(y,x)
• freePropagator_smooth, freePropagator_complex_smooth: Smoothness results
• freePropagator_pos, freePropagator_bounded: Propagator is positive and bounded

No axioms declared in this file.

Small helper lemmas for integration and complex algebra

theorem integral_ofReal_eq {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (h : α → ℝ) (_hf : MeasureTheory.Integrable h μ) : ∫ (x : α), ↑(h x) ∂μ = ↑(∫ (x : α), h x ∂μ)

Helper theorem: integral of a real-valued function, coerced to ℂ, equals ofReal of the real integral.

theorem schwartz_L2_integrable (f : TestFunctionℂ) : MeasureTheory.Integrable (fun (k : SpaceTime) => ‖f k‖ ^ 2) MeasureTheory.volume

Helper lemma: Schwartz functions are L²-integrable.

theorem integral_const_mul {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ℝ) (f : α → ℝ) (hf : MeasureTheory.Integrable f μ) : MeasureTheory.Integrable (fun (x : α) => c * f x) μ

Helper theorem: Integrability is preserved by multiplying a real integrand with a real constant.

theorem integral_const_mul_eq {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (c : ℝ) (f : α → ℝ) (_hf : MeasureTheory.Integrable f μ) : ∫ (x : α), c * f x ∂μ = c * ∫ (x : α), f x ∂μ

Helper theorem: Integral of a real constant multiple pulls out of the integral.

theorem real_integral_mono_of_le {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (f g : α → ℝ) (hg : MeasureTheory.Integrable g μ) (hf_nonneg : ∀ (x : α), 0 ≤ f x) (hle : ∀ (x : α), f x ≤ g x) : ∫ (x : α), f x ∂μ ≤ ∫ (x : α), g x ∂μ

Helper theorem: Monotonicity of the real integral for pointwise ≤ between nonnegative functions, assuming the larger one is integrable.

Free Covariance in Euclidean QFT

The free covariance is the fundamental two-point correlation function for the Gaussian Free Field. In Euclidean spacetime, it is given by the Fourier transform:

C(x,y) = ∫ (d^d k)/(2π)^d * 1/(k² + m²) * exp(-i k·(x-y))

where:

• m > 0 is the mass parameter
• k² = k·k is the Euclidean norm squared (using inner product ⟨k,k⟩)
• d is the spacetime dimension

This defines a positive definite bilinear form, which is essential for reflection positivity.

Key point: In Lean, we can use ⟨x, y⟩ for the inner product and ‖x‖ for the norm.

noncomputable def freePropagatorMomentum (m : ℝ) (k : SpaceTime) : ℝ

The free propagator in momentum space: 1/(k² + m²) This is the Fourier transform of the free covariance

Equations

• freePropagatorMomentum m k = 1 / (‖k‖ ^ 2 + m ^ 2)

theorem freePropagator_even (m : ℝ) (k : SpaceTime) : freePropagatorMomentum m (-k) = freePropagatorMomentum m k

The free propagator is an even function: it depends only on ‖k‖.

noncomputable def freePropagatorMomentumMathlib (m : ℝ) (k : SpaceTime) : ℝ

The propagator in "Mathlib momentum coordinates". When using Mathlib's Fourier transform convention, the propagator acquires (2π)² factors. This is P_mathlib(k) = 1/((2π)²‖k‖² + m²) which equals P_phys(2πk).

Equations

• freePropagatorMomentumMathlib m k = 1 / ((2 * Real.pi) ^ 2 * ‖k‖ ^ 2 + m ^ 2)

theorem freePropagatorMomentum_mathlib_pos (m : ℝ) (hm : 0 < m) (k : SpaceTime) : 0 < freePropagatorMomentumMathlib m k

The Mathlib propagator is positive for m > 0.

theorem freePropagatorMomentum_mathlib_nonneg (m : ℝ) (hm : 0 < m) (k : SpaceTime) : 0 ≤ freePropagatorMomentumMathlib m k

The Mathlib propagator is non-negative.

noncomputable def freeCovarianceRegulated (α m : ℝ) (x y : SpaceTime) : ℝ

The regulated free covariance kernel in position space. This is the Fourier transform of the momentum space propagator with Gaussian regulator:

C_α(x,y) = ∫ \frac{d^d k}{(2π)^d}; \frac{e^{-α‖k‖²} e^{-i k·(x-y)}}{‖k‖² + m²}.

The regulator exp(-α‖k‖²) with α > 0 makes the integral absolutely convergent. In the limit α → 0⁺, this recovers the (conditionally convergent) Fourier integral which equals the Bessel form.

We realise this as the real part of a complex Fourier integral with the standard 2π-normalisation.

Equations

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

Schwinger Representation of the Propagator

The Schwinger (or proper-time) representation expresses the massive propagator as:

1/(k² + m²) = ∫₀^∞ exp(-t(k² + m²)) dt

This integral is absolutely convergent for k² + m² > 0. The key insight is that this converts the Fourier transform of the propagator into a Gaussian integral, which can be computed explicitly using Mathlib's fourierIntegral_gaussian_innerProductSpace.

After applying the Gaussian Fourier transform, we get:

∫ dk e^{-ik·r} / (k² + m²) = ∫₀^∞ e^{-tm²} · (π/t)^{d/2} · e^{-r²/(4t)} dt / (2π)^d

In 4D (d=4), this simplifies to:

C(r) = (1/(16π²)) ∫₀^∞ e^{-tm²} · (1/t²) · e^{-r²/(4t)} dt

The remaining 1D integral can be computed via the substitution u = m²t + r²/(4t), which leads to the Bessel K₁ function.

noncomputable def schwingerIntegrand (t m : ℝ) (k : SpaceTime) : ℝ

The Schwinger integrand: exp(-t(k² + m²)) for t > 0. Integrating this over t ∈ (0, ∞) gives 1/(k² + m²).

Equations

• schwingerIntegrand t m k = Real.exp (-t * (‖k‖ ^ 2 + m ^ 2))

theorem integral_exp_neg_mul_Ioi_eq_inv (a : ℝ) (ha : 0 < a) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-a * t) = 1 / a

Integral of exp(-a*t) over (0, ∞) equals 1/a for a > 0. This is the Laplace transform of 1 at parameter a. Proof: Change of variables u = at gives (1/a) ∫₀^∞ e^{-u} du = 1/a.

theorem schwinger_representation (m : ℝ) (hm : 0 < m) (k : SpaceTime) : ∫ (t : ℝ) in Set.Ioi 0, schwingerIntegrand t m k = 1 / (‖k‖ ^ 2 + m ^ 2)

The Schwinger representation: ∫₀^∞ exp(-t(k² + m²)) dt = 1/(k² + m²). This is valid when k² + m² > 0.

noncomputable def schwingerGaussian (α t m : ℝ) (k : SpaceTime) : ℝ

The combined Gaussian factor for the Schwinger-regulated integral. This combines the propagator Schwinger factor with the UV regulator.

Equations

• schwingerGaussian α t m k = Real.exp (-(α + t) * ‖k‖ ^ 2 - t * m ^ 2)

noncomputable def heatKernelPositionSpace (t r : ℝ) : ℝ

The heat kernel in d dimensions for position space: (4πt)^{-d/2} · exp(-r²/(4t)). This is the Fourier transform of the Gaussian exp(-t·k²). Named with PositionSpace suffix to distinguish from momentum-space version.

Equations

• heatKernelPositionSpace t r = (4 * Real.pi * t) ^ (-↑STDimension / 2) * Real.exp (-r ^ 2 / (4 * t))

theorem heatKernelPositionSpace_4D (t : ℝ) (ht : 0 < t) (r : ℝ) : heatKernelPositionSpace t r = 1 / (16 * Real.pi ^ 2 * t ^ 2) * Real.exp (-r ^ 2 / (4 * t))

For d = 4, the heat kernel simplifies to 1/(16π²t²) · exp(-r²/(4t)).

theorem heatKernelPositionSpace_nonneg (t : ℝ) (ht : 0 < t) (r : ℝ) : 0 ≤ heatKernelPositionSpace t r

The heat kernel is nonnegative.

theorem heatKernelPositionSpace_continuous_at (t : ℝ) (ht : 0 < t) (r : ℝ) : ContinuousAt (fun (s : ℝ) => heatKernelPositionSpace s r) t

The heat kernel is continuous in t for t > 0.

theorem heatKernelPositionSpace_bounded (r : ℝ) (hr : 0 < r) : ∃ (C : ℝ), 0 < C ∧ ∀ s > 0, heatKernelPositionSpace s r ≤ C

The heat kernel is bounded by a constant depending only on r > 0. Maximum of H(s,r) = (4πs)^{-d/2} exp(-r²/(4s)) occurs at s = r²/(2d).

theorem heatKernelPositionSpace_integral_eq_one (t : ℝ) (ht : 0 < t) : ∫ (z : SpaceTime), heatKernelPositionSpace t ‖z‖ = 1

Heat kernel L¹ normalization: The heat kernel integrates to 1 over all space. ∫ H(t, ‖z‖) dz = 1 for all t > 0.

This is a fundamental property of the heat kernel as the Green's function for the heat equation with conservation of total probability/mass.

Proof: Uses integral_rexp_neg_mul_sq_norm from Mathlib: ∫ exp(-b‖v‖²) dv = (π/b)^{d/2}

With b = 1/(4t) and d = 4: ∫ (4πt)^{-2} exp(-‖z‖²/(4t)) dz = (4πt)^{-2} × (4πt)² = 1

noncomputable def covarianceSchwingerRep (m r : ℝ) : ℝ

The Schwinger representation of the position-space covariance. This expresses C(r) as a 1D integral over proper time.

Equations

• covarianceSchwingerRep m r = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t * m ^ 2) * heatKernelPositionSpace t r

theorem covarianceSchwingerRep_4D (m : ℝ) (_hm : 0 < m) (r : ℝ) (_hr : 0 < r) : covarianceSchwingerRep m r = 1 / (16 * Real.pi ^ 2) * ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t * m ^ 2) * (1 / t ^ 2) * Real.exp (-r ^ 2 / (4 * t))

In 4D, the Schwinger representation of the covariance equals: (1/(16π²)) ∫₀^∞ exp(-tm²) · (1/t²) · exp(-r²/(4t)) dt

theorem covarianceSchwingerRep_eq_besselFormula (m r : ℝ) (hm : 0 < m) (hr : 0 < r) : covarianceSchwingerRep m r = m / (4 * Real.pi ^ 2 * r) * besselK1 (m * r)

The Schwinger representation of the covariance equals the Bessel formula. C(r) = covarianceSchwingerRep m r = (m/(4π²r)) K₁(mr)

This is the main result connecting the Schwinger proper-time representation to the explicit Bessel function formula for the free scalar propagator in 4D.

noncomputable def freeCovarianceBessel (m : ℝ) (x y : SpaceTime) : ℝ

The free covariance in position space via Bessel function representation. C(x,y) = (m / (4π² |x-y|)) · K₁(m |x-y|)

This is the explicit formula for the massive scalar field propagator in 4D. The formula is valid for x ≠ y and m > 0.

Equations

• freeCovarianceBessel m x y = if ‖x - y‖ = 0 then 0 else m / (4 * Real.pi ^ 2 * ‖x - y‖) * besselK1 (m * ‖x - y‖)

@[reducible, inline]

noncomputable abbrev freeCovariance (m : ℝ) (x y : SpaceTime) : ℝ

The free covariance in position space (abbreviation for the Bessel representation).

Equations

• freeCovariance m x y = freeCovarianceBessel m x y

theorem freeCovarianceBessel_symm (m : ℝ) (x y : SpaceTime) : freeCovarianceBessel m x y = freeCovarianceBessel m y x

The Bessel covariance is symmetric.

theorem freeCovarianceBessel_pos (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) : 0 < freeCovarianceBessel m x y

The Bessel covariance is positive for distinct points and m > 0.

Connecting Fourier Representation to Schwinger Representation

The key to proving that the regulated Fourier integral converges to the Bessel form is to use the Schwinger representation as an intermediate step:

1. Fubini step: Exchange the k-integral (Fourier) with the t-integral (Schwinger) ∫ dk e^{-α‖k‖²} e^{-ik·r} / (k² + m²) = ∫₀^∞ dt e^{-tm²} [∫ dk e^{-(α+t)‖k‖²} e^{-ik·r}]

2. Gaussian FT: The inner k-integral is a Gaussian Fourier transform ∫ dk e^{-s‖k‖²} e^{-ik·r} = (π/s)^{d/2} e^{-r²/(4s)} (from Mathlib)

3. Limit α → 0: The regulated integral converges to the unregulated Schwinger form ∫₀^∞ dt e^{-tm²} H(t,r) = covarianceSchwingerRep m r

4. Bessel connection: By covarianceSchwingerRep_eq_besselFormula, this equals (m/(4π²r)) K₁(mr) = freeCovarianceBessel m x y

noncomputable def covarianceSchwingerRegulated (α m r : ℝ) : ℝ

The Schwinger-regulated covariance: uses proper-time representation with regulator α. C_α^{Schwinger}(r) = ∫₀^∞ e^{-tm²} H(α+t, r) dt where H(s,r) = (4πs)^{-d/2} e^{-r²/(4s)} is the heat kernel.

This is an intermediate form between the Fourier representation and the Bessel form.

Equations

• covarianceSchwingerRegulated α m r = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t * m ^ 2) * heatKernelPositionSpace (α + t) r

theorem integrableOn_exp_neg_mul_sq_Ioi (m : ℝ) (hm : 0 < m) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-t * m ^ 2)) (Set.Ioi 0) MeasureTheory.volume

Integrability of exp(-tm²) on (0, ∞) for m > 0.

theorem integrableOn_exp_neg_mul_sq_const_Ioi (m : ℝ) (hm : 0 < m) (C : ℝ) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (-t * m ^ 2) * C) (Set.Ioi 0) MeasureTheory.volume

Integrability of exp(-tm²) * C on (0, ∞) for m > 0 and any constant C.

theorem gaussianFT_eq_heatKernel_times_norm (s : ℝ) (hs : 0 < s) (z : SpaceTime) : ∫ (k : SpaceTime), Complex.exp (-↑s * ↑‖k‖ ^ 2) * Complex.exp (-Complex.I * ↑(inner ℝ k z)) = ↑((2 * Real.pi) ^ STDimension) * ↑(heatKernelPositionSpace s ‖z‖)

The Gaussian Fourier transform gives the heat kernel (times normalization). ∫_k e^{-s‖k‖²} e^{-ik·z} dk = (2π)^d H(s, ‖z‖)

This is the key identity connecting momentum and position space.

theorem integrable_schwinger_fourier_integrand (α : ℝ) (hα : 0 < α) (m : ℝ) (hm : 0 < m) : MeasureTheory.Integrable (fun (p : SpaceTime × ℝ) => if p.2 > 0 then Real.exp (-(α + p.2) * ‖p.1‖ ^ 2 - p.2 * m ^ 2) else 0) (MeasureTheory.volume.prod MeasureTheory.volume)

THEOREM: The integrand for fubini_schwinger_fourier is integrable on SpaceTime × (0,∞). This justifies using Tonelli's theorem.

Proof:

• The integrand factors as exp(-(α+t)‖k‖²) × exp(-tm²)
• For k: ∫ exp(-(α+t)‖k‖²) dk is finite (Gaussian integral, since α+t > α > 0)
• For t: ∫_0^∞ exp(-tm²) dt = 1/m² (exponential integral)
• The product integral converges by Tonelli since all terms are non-negative

theorem fubini_schwinger_integrand (α : ℝ) (hα : 0 < α) (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (_hxy : x ≠ y) : (∫ (k : SpaceTime), ↑(∫ (t : ℝ) in Set.Ioi 0, Real.exp (-(α + t) * ‖k‖ ^ 2) * Real.exp (-t * m ^ 2)) * Complex.exp (-Complex.I * ↑(inner ℝ k (x - y)))).re = ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t * m ^ 2) * (∫ (k : SpaceTime), Complex.exp (-↑(α + t) * ↑‖k‖ ^ 2) * Complex.exp (-Complex.I * ↑(inner ℝ k (x - y)))).re

Fubini swap lemma for the Schwinger integrand with phase.

This lemma asserts that the integration order can be swapped for the Gaussian × phase integrand appearing in the Schwinger representation:

Re[∫_k (∫_t exp(-(α+t)‖k‖²) * exp(-tm²) dt) * phase(k) dk] = ∫_t exp(-tm²) * Re[∫_k exp(-(α+t)‖k‖²) * phase(k) dk] dt

Justification: Both sides are the same double integral of exp(-(α+t)‖k‖² - tm²) * exp(-i⟪k, x-y⟫) with integration order swapped. Fubini applies because the absolute value is integrable (the phase has norm 1).

This follows from MeasureTheory.integral_integral_swap together with integrability bounds from the Gaussian decay.

theorem fubini_schwinger_fourier (α : ℝ) (hα : 0 < α) (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) : freeCovarianceRegulated α m x y = covarianceSchwingerRegulated α m ‖x - y‖

The regulated Fourier integral equals the Schwinger-regulated form via Fubini/Tonelli.

theorem covarianceSchwingerRegulated_tendsto (m : ℝ) (hm : 0 < m) (r : ℝ) (hr : 0 < r) : Filter.Tendsto (fun (α : ℝ) => covarianceSchwingerRegulated α m r) (nhdsWithin 0 (Set.Ioi 0)) (nhds (covarianceSchwingerRep m r))

As α → 0⁺, the Schwinger-regulated covariance converges to the unregulated form.

theorem covarianceSchwingerRep_eq_freeCovarianceBessel (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) : covarianceSchwingerRep m ‖x - y‖ = freeCovarianceBessel m x y

The unregulated Schwinger form equals the Bessel form (for r > 0).

theorem freeCovariance_regulated_tendsto_bessel (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) : Filter.Tendsto (fun (α : ℝ) => freeCovarianceRegulated α m x y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (freeCovarianceBessel m x y))

Main theorem: The regulated Fourier covariance converges to the Bessel form. This follows from the Schwinger representation approach:

1. Use fubini_schwinger_fourier to convert Fourier → Schwinger
2. Use covarianceSchwingerRegulated_tendsto for the α → 0 limit
3. Use covarianceSchwingerRep_eq_freeCovarianceBessel for Schwinger → Bessel

theorem freeCovariance_regulated_limit_eq_freeCovariance (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) : Filter.Tendsto (fun (α : ℝ) => freeCovarianceRegulated α m x y) (nhdsWithin 0 (Set.Ioi 0)) (nhds (freeCovariance m x y))

The deep result: The regulated Fourier integral converges to the Bessel form as α → 0⁺. This is the statement that the Fourier transform of 1/(k² + m²) in 4D equals (m / (4π² r)) · K₁(mr).

The proof involves:

1. Reducing to a 1D integral by exploiting rotational symmetry
2. Computing the Fourier transform of a radial function in 4D
3. Using the integral representation of K₁
4. Taking the limit α → 0⁺ of the regulated integral

The regulator exp(-α‖k‖²) makes the integral absolutely convergent for any α > 0. The limit exists and equals the Bessel form for x ≠ y.

theorem covarianceSchwingerRegulated_le_const_mul (m : ℝ) (hm : 0 < m) (r : ℝ) (hr : 0 < r) (α : ℝ) (hα : 0 < α) (hα1 : α ≤ 1) : covarianceSchwingerRegulated α m r ≤ Real.exp (m ^ 2) * covarianceSchwingerRep m r

Domination bound (Schwinger): The Schwinger-regulated covariance is bounded by a constant times the unregulated form. For α ∈ (0, 1], we have: C_regulated(α, m, r) ≤ exp(m²) × C_Bessel(m, r)

Proof: Using change of variables s = α + t: C_regulated = ∫₀^∞ exp(-tm²) H(α+t, r) dt = ∫_α^∞ exp(-(s-α)m²) H(s, r) ds (substitute s = α + t) = exp(αm²) × ∫_α^∞ exp(-sm²) H(s, r) ds ≤ exp(αm²) × ∫₀^∞ exp(-sm²) H(s, r) ds (since integrand ≥ 0) = exp(αm²) × C_Bessel(m, r) ≤ exp(m²) × C_Bessel(m, r) (for α ≤ 1)

theorem freeCovariance_regulated_le_const_mul_freeCovariance (m : ℝ) (hm : 0 < m) (x y : SpaceTime) (hxy : x ≠ y) (α : ℝ) (hα : 0 < α) (hα1 : α ≤ 1) : |freeCovarianceRegulated α m x y| ≤ Real.exp (m ^ 2) * freeCovariance m x y

Domination bound: For α ∈ (0, 1] and x ≠ y, the regulated covariance is bounded by a constant times the Bessel form: |freeCovarianceRegulated α m x y| ≤ exp(m²) × freeCovariance m x y

This bound enables dominated convergence for the bilinear form.

theorem gaussian_regulator_integrable' (α : ℝ) (hα : 0 < α) : MeasureTheory.Integrable (fun (k : SpaceTime) => Real.exp (-α * ‖k‖ ^ 2)) MeasureTheory.volume

The Gaussian regulator exp(-α‖k‖²) is integrable on SpaceTime for α > 0.

theorem freeCovariance_regulated_uniformly_bounded (α : ℝ) (hα : 0 < α) (m : ℝ) (hm : 0 < m) : ∃ M > 0, ∀ (x y : SpaceTime), |freeCovarianceRegulated α m x y| ≤ M

The regulated covariance is uniformly bounded for all (x, y).

Since |exp(-ik·(x-y))| = 1 and the Gaussian-regulated propagator is integrable, we have |C_α(x,y)| ≤ ∫ exp(-α‖k‖²) * P(k) / (2π)^d ≤ ∫ exp(-α‖k‖²) / (m² (2π)^d) < ∞.

Proof sketch:

• The Fourier integrand has |phase| = 1 and |amplitude| ≤ exp(-α‖k‖²)/(m²(2π)^d)
• The Gaussian is integrable, giving the uniform bound M = ∫ exp(-α‖k‖²)/(m²(2π)^d) dk
• Since C_α is the real part of the integral, |C_α| ≤ M for all (x,y)

theorem aestronglyMeasurable_freeCovariance_regulated (α : ℝ) (hα : 0 < α) (m : ℝ) (hm : 0 < m) : MeasureTheory.AEStronglyMeasurable (fun (p : SpaceTime × SpaceTime) => ↑(freeCovarianceRegulated α m p.1 p.2)) (MeasureTheory.volume.prod MeasureTheory.volume)

The regulated covariance is AEStronglyMeasurable on the product space.

Proof: The Schwinger representation is an integral ∫_k exp(-α‖k‖²) * prop(k) * cos(k·(x-y)). The integrand is continuous in (x, y) for fixed k, hence measurable. By Fubini theorem structure, the integral inherits measurability in (x, y).

theorem aestronglyMeasurable_freeCovariance (m : ℝ) [Fact (0 < m)] : MeasureTheory.AEStronglyMeasurable (fun (p : SpaceTime × SpaceTime) => ↑(freeCovariance m p.1 p.2)) (MeasureTheory.volume.prod MeasureTheory.volume)

The unregulated Bessel covariance is AEStronglyMeasurable on the product space.

Proof: The Bessel covariance is continuous on the off-diagonal set {(x,y) | x ≠ y}, which has full measure in the product space (diagonal has measure zero). Continuity implies strong measurability, hence AEStronglyMeasurable.

theorem freeCovariance_regulated_bilinear_integrable (α : ℝ) (hα : 0 < α) (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : MeasureTheory.Integrable (fun (p : SpaceTime × SpaceTime) => f p.1 * ↑(freeCovarianceRegulated α m p.1 p.2) * g p.2) MeasureTheory.volume

The bilinear form f(x) * C_α(x,y) * g(y) is integrable for regulated covariance with Schwartz f, g.

Since C_α is uniformly bounded and f, g are Schwartz (hence integrable), the product is
integrable.

**Proof:** With bound M from `freeCovariance_regulated_uniformly_bounded`:
|f(x) * C_α(x,y) * g(y)| ≤ M * |f(x)| * |g(y)|
The RHS is integrable since f, g ∈ L¹ (Schwartz functions are integrable).

noncomputable def freeCovarianceKernel (m : ℝ) (z : SpaceTime) : ℝ

The free covariance kernel (alternative name for compatibility)

Equations

• freeCovarianceKernel m z = freeCovariance m 0 z

theorem freeCovarianceKernel_integrable (m : ℝ) (hm : 0 < m) : MeasureTheory.Integrable (freeCovarianceKernel m) MeasureTheory.volume

The Bessel covariance kernel is L¹ (integrable on SpaceTime).

In d=4 dimensions with f(r) = (m/(4π²r)) K₁(mr): ∫_{ℝ⁴} |K(z)| dz ↔ ∫₀^∞ r³ |f(r)| dr = (m/4π²) ∫₀^∞ r² K₁(mr) dr

This is finite by radial_besselK1_integrable.

theorem freeCovarianceKernel_decay_bound (m : ℝ) (hm : 0 < m) : ∃ C > 0, ∀ (z : SpaceTime), |freeCovarianceKernel m z| ≤ C * ‖z‖ ^ (-2)

Polynomial decay bound for the free covariance kernel.

The free covariance kernel satisfies |C(z)| ≤ C/‖z‖² for some C > 0.

This uses the Bessel function bounds:

• Near origin (mr ≤ 1): K₁(mr) ≤ (cosh(1) + 2)/(mr), giving C(z) ≤ (cosh(1)+2)/(4π²r²)
• Far from origin (mr > 1): K₁(mr) ≤ (sinh(1) + 2)·exp(-mr), decays faster than 1/r²

The bound is essential for OS1 local integrability in d=4 dimensions.

theorem freeCovariance_exponential_bound (m : ℝ) (hm : 0 < m) (u v : SpaceTime) (h_sep : 1 ≤ m * ‖u - v‖) : |freeCovariance m u v| ≤ m ^ 2 * (Real.sinh 1 + 2) / (4 * Real.pi ^ 2) * Real.exp (-m * ‖u - v‖)

Exponential decay bound for the free covariance.

For m > 0 and u, v ∈ ℝ⁴ with m‖u - v‖ ≥ 1: |C(u, v)| ≤ (m² · (sinh 1 + 2) / (4π²)) · e^{-m‖u-v‖}

This combines:

• The covariance formula: C(u,v) = (m / (4π² ‖u-v‖)) · K₁(m‖u-v‖)
• The Bessel asymptotic: K₁(z) ≤ (sinh 1 + 2) · e^{-z} for z ≥ 1
• The condition m‖u-v‖ ≥ 1, which implies ‖u-v‖ ≥ 1/m, so m/‖u-v‖ ≤ m²

Fact versions of decay bounds

These are convenience wrappers that use [Fact (0 < m)] instead of explicit (hm : 0 < m), for compatibility with code that uses the Fact type class.

theorem freeCovariance_exponential_bound' (m : ℝ) [Fact (0 < m)] (u v : SpaceTime) (h_sep : 1 ≤ m * ‖u - v‖) : |freeCovariance m u v| ≤ m ^ 2 * (Real.sinh 1 + 2) / (4 * Real.pi ^ 2) * Real.exp (-m * ‖u - v‖)

Exponential bound with [Fact (0 < m)] type class.

theorem freeCovarianceKernel_continuousOn (m : ℝ) (hm : 0 < m) : ContinuousOn (freeCovarianceKernel m) {z : SpaceTime | z ≠ 0}

Continuity of the free covariance kernel away from the origin.

The kernel C(z) = (m/(4π²‖z‖)) K₁(m‖z‖) is continuous on {z | z ≠ 0}.

This follows from:

• ‖z‖ is continuous
• K₁ is continuous on (0, ∞) (see besselK1_continuousOn)
• Division by ‖z‖ is continuous for z ≠ 0

This is essential for the double mollifier convergence theorem.

theorem freeCovarianceℂ_bilinear_integrable' (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : MeasureTheory.Integrable (fun (p : SpaceTime × SpaceTime) => f p.1 * ↑(freeCovariance m p.1 p.2) * g p.2) MeasureTheory.volume

The bilinear form f(x) * C(x,y) * g(y) is integrable on product space for Schwartz f, g. This uses the L¹ integrability of the translation-invariant Bessel kernel.

def negSpaceTime : SpaceTime ≃ₗᵢ[ℝ] SpaceTime

Negation as a linear isometry equivalence on SpaceTime.

Equations

• negSpaceTime = { toLinearEquiv := LinearEquiv.neg ℝ, norm_map' := negSpaceTime._proof_1 }

theorem integral_comp_neg_spacetime {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f : SpaceTime → E) : ∫ (k : SpaceTime), f (-k) = ∫ (k : SpaceTime), f k

Helper lemma: Integral with change of variables k ↦ -k for SpaceTime. This uses that linear isometries preserve measure on finite-dimensional inner product spaces.

theorem freeCovariance_symmetric (m : ℝ) (x y : SpaceTime) : freeCovariance m x y = freeCovariance m y x

Position-space free covariance is symmetric: C(x,y) = C(y,x).

theorem freeCovariance_star (m : ℝ) (x y : SpaceTime) : star ↑(freeCovariance m x y) = ↑(freeCovariance m x y)

The position-space free covariance is real-valued after ℂ coercion.

theorem freeCovariance_hermitian (m : ℝ) (x y : SpaceTime) : ↑(freeCovariance m x y) = star ↑(freeCovariance m y x)

Hermiticity of the complex-lifted position-space kernel.

theorem freePropagator_smooth (m : ℝ) [Fact (0 < m)] : ContDiff ℝ ↑⊤ fun (k : SpaceTime) => freePropagatorMomentum m k

The free propagator function is smooth (infinitely differentiable).

theorem freePropagator_complex_smooth (m : ℝ) [Fact (0 < m)] : ContDiff ℝ ↑⊤ fun (k : SpaceTime) => ↑(freePropagatorMomentum m k)

The complex-valued free propagator function is smooth.

theorem freePropagator_pos {m : ℝ} [Fact (0 < m)] (k : SpaceTime) : 0 < freePropagatorMomentum m k

The free propagator is positive

theorem freePropagator_bounded {m : ℝ} [Fact (0 < m)] (k : SpaceTime) : freePropagatorMomentum m k ≤ 1 / m ^ 2

The free propagator is bounded above by 1/m²

theorem freePropagator_continuous {m : ℝ} [Fact (0 < m)] : Continuous (freePropagatorMomentum m)

The free propagator is continuous

Complex conjugation properties of the propagator

@[simp]

theorem freePropagatorMomentum_star (m : ℝ) (k : SpaceTime) : star ↑(freePropagatorMomentum m k) = ↑(freePropagatorMomentum m k)

The momentum-space propagator is real-valued: its star (complex conjugate) equals itself.

theorem freePropagatorMomentum_starRing (m : ℝ) (k : SpaceTime) : (starRingEnd ℂ) ↑(freePropagatorMomentum m k) = ↑(freePropagatorMomentum m k)

Same statement via the star ring endomorphism (complex conjugate).

@[simp]

theorem freePropagatorMomentum_im (m : ℝ) (k : SpaceTime) : (↑(freePropagatorMomentum m k)).im = 0

In particular, the imaginary part of the momentum-space propagator vanishes.

Momentum weight functions for L² embedding

noncomputable def momentumWeight (m : ℝ) (k : SpaceTime) : ℝ

The weight function in momentum space (physics convention): 1 / (‖k‖² + m²)

Equations

• momentumWeight m k = 1 / (‖k‖ ^ 2 + m ^ 2)

noncomputable def momentumWeightMathlib (m : ℝ) (k : SpaceTime) : ℝ

The weight function in momentum space (Mathlib convention): 1 / ((2π)²‖k‖² + m²) This is the correct weight to use with Mathlib's Fourier transform.

Equations

• momentumWeightMathlib m k = freePropagatorMomentumMathlib m k

noncomputable def momentumWeightSqrt (m : ℝ) (k : SpaceTime) : ℝ

The square root of the weight function (physics convention).

Equations

• momentumWeightSqrt m k = 1 / √(‖k‖ ^ 2 + m ^ 2)

noncomputable def momentumWeightSqrtMathlib (m : ℝ) (k : SpaceTime) : ℝ

The square root of the weight function (Mathlib convention). This is the correct weight to use with Mathlib's Fourier transform.

Equations

• momentumWeightSqrtMathlib m k = 1 / √((2 * Real.pi) ^ 2 * ‖k‖ ^ 2 + m ^ 2)

theorem momentumWeightSqrt_mathlib_pos (m : ℝ) [Fact (0 < m)] (k : SpaceTime) : 0 < momentumWeightSqrtMathlib m k

The square root weight is positive (Mathlib convention).

theorem momentumWeightSqrt_mathlib_sq (m : ℝ) [Fact (0 < m)] (k : SpaceTime) : momentumWeightSqrtMathlib m k ^ 2 = momentumWeightMathlib m k

The square of the sqrt weight equals the weight (Mathlib convention).

theorem momentumWeightSqrt_continuous (m : ℝ) [Fact (0 < m)] : Continuous fun (k : SpaceTime) => momentumWeightSqrt m k

The momentum weight sqrt function is continuous (physics convention).

theorem momentumWeightSqrt_mathlib_continuous (m : ℝ) [Fact (0 < m)] : Continuous fun (k : SpaceTime) => momentumWeightSqrtMathlib m k

The momentum weight sqrt function is continuous (Mathlib convention).

theorem momentumWeightSqrt_measurable (m : ℝ) [Fact (0 < m)] : Measurable fun (k : SpaceTime) => momentumWeightSqrt m k

The momentum weight sqrt function is measurable (physics convention).

theorem momentumWeightSqrt_mathlib_measurable (m : ℝ) [Fact (0 < m)] : Measurable fun (k : SpaceTime) => momentumWeightSqrtMathlib m k

The momentum weight sqrt function is measurable (Mathlib convention).

theorem momentumWeightSqrt_bounded_ae (m : ℝ) [Fact (0 < m)] : ∀ᵐ (k : SpaceTime), ‖↑(momentumWeightSqrt m k)‖ ≤ 1 / m

Helper: The weight function as an L^∞ function (essentially bounded).

theorem momentumWeightSqrt_mathlib_bounded_ae (m : ℝ) [Fact (0 < m)] : ∀ᵐ (k : SpaceTime), ‖↑(momentumWeightSqrtMathlib m k)‖ ≤ 1 / m

Helper: The mathlib weight function as an L^∞ function (essentially bounded).

noncomputable def momentumWeightSqrtMulCLM (m : ℝ) [Fact (0 < m)] : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Multiplication by the square-root momentum weight defines a bounded linear operator on complex L² (physics convention).

Equations

• momentumWeightSqrtMulCLM m = linftyMulL2CLM (fun (k : SpaceTime) => ↑(momentumWeightSqrt m k)) ⋯ (1 / m) ⋯

noncomputable def momentumWeightSqrtMathlibMulCLM (m : ℝ) [Fact (0 < m)] : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Multiplication by the square-root momentum weight defines a bounded linear operator on complex L² (Mathlib convention).

Equations

• momentumWeightSqrtMathlibMulCLM m = linftyMulL2CLM (fun (k : SpaceTime) => ↑(momentumWeightSqrtMathlib m k)) ⋯ (1 / m) ⋯

theorem momentumWeightSqrt_mathlib_mul_CLM_spec (m : ℝ) [Fact (0 < m)] (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↑↑((momentumWeightSqrtMathlibMulCLM m) f) =ᵐ[MeasureTheory.volume] fun (k : SpaceTime) => ↑(momentumWeightSqrtMathlib m k) * ↑↑f k

theorem momentumWeightSqrt_mathlib_le_inv_mass (m : ℝ) [Fact (0 < m)] (k : SpaceTime) : momentumWeightSqrtMathlib m k ≤ 1 / m

The square-root momentum weight is pointwise bounded by 1 / m (Mathlib convention).