Position-Space Free Covariance

Position-space covariance C(x,y) = (m/4π²|x−y|) K₁(m|x−y|) and its properties: Euclidean invariance, time reflection invariance, and Schwinger representation C(x,y) = ∫₀^∞ e^{−sm²} H(s,|x−y|) ds via the heat kernel.

Main definitions

• freeCovarianceℂBilinear: bilinear form ⟨f, Cg⟩ = ∫∫ f(x) C(x,y) g(y) dx dy

Key Results

• freeCovariance_euclidean_invariant: Euclidean invariance of the covariance
• covariance_timeReflection_invariant: Time reflection invariance

Dependencies

No axioms declared here. Uses freeCovarianceℂ_bilinear_integrable transitively via parseval_triple_integrand_integrable in Covariance.Parseval.

theorem parseval_covariance_schwartz_regulated' (α : ℝ) (hα : 0 < α) (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : (∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovarianceRegulated α m x y) * (starRingEnd ℂ) (f y)).re = ∫ (k : SpaceTime), Real.exp (-α * (2 * Real.pi) ^ 2 * ‖k‖ ^ 2) * ‖((SchwartzMap.fourierTransformCLM ℂ) f) k‖ ^ 2 * freePropagatorMomentumMathlib m k

** (Parseval for Covariance - Position Space formulation with regulator):** The fundamental Parseval identity relating the regulated covariance bilinear form to momentum-space propagator. The regulator exp(-α(2π)²‖k‖²) ensures absolute convergence.

Uses freePropagatorMomentumMathlib which accounts for the 2π factor in Mathlib's Fourier convention. Defined in FourierTransforms.lean as parseval_covariance_schwartz_regulated.

theorem double_integral_timeReflection (G : SpaceTime → SpaceTime → ℂ) (_hG : MeasureTheory.Integrable (fun (p : SpaceTime × SpaceTime) => G p.1 p.2) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (x : SpaceTime) (y : SpaceTime), G (QFT.timeReflection x) (QFT.timeReflection y) = ∫ (x : SpaceTime) (y : SpaceTime), G x y

(Time Reflection Change of Variables): Integrating a function over spacetime is unchanged when both variables are composed with geometric time reflection. This packages the measure-preserving property of time reflection together with Fubini's theorem for later use in reflection-positivity arguments.

theorem double_integral_timeReflection_covariance (m : ℝ) (f g : TestFunctionℂ) (hf : MeasureTheory.Integrable (fun (p : SpaceTime × SpaceTime) => (QFT.compTimeReflection f) p.1 * ↑(freeCovariance m p.1 p.2) * g p.2) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (x : SpaceTime) (y : SpaceTime), (QFT.compTimeReflection f) x * ↑(freeCovariance m x y) * g y = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovariance m (QFT.timeReflection x) (QFT.timeReflection y)) * (QFT.compTimeReflection g) y

Specialized time-reflection change of variables for covariance-type kernels. This packages the combination of double_integral_timeReflection and the observation that compTimeReflection is just composition with timeReflection, so we can reuse the general measure-preserving lemma without re-establishing integrability each time.

Reflection Positivity for Free Covariance

For real test functions supported on positive time (t > 0), the cross-covariance ∫∫ (Θf)(x) C(x,y) f(y) dx dy ≥ 0 where Θ is time reflection.

Mathematical justification: In momentum space, the free covariance factorizes as C(x,y) = ∫ e^{ik·(x-y)} / (k² + m²) dk. For functions with positive time support, the time integral factorizes via contour integration, yielding an exponential e^{-ω|t|} factor (where ω = √(|p|² + m²)) which ensures the cross-term is positive.

This is the key input for Osterwalder-Schrader reflection positivity (OS3).

PROVEN: See QFT.freeCovariance_reflection_positive_bilinear in CovarianceRP.lean, which uses the direct momentum representation approach (RPProof namespace).

Complex Bilinear Form on Test Functions

The following section develops the bilinear structure of the covariance form. All results assume m > 0 (positive mass) which is required for integrability.

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 position-space integrand for the complex covariance bilinear form is integrable for Schwartz test functions, using translation-invariant L¹ kernel integrability.

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

Integrability of the covariance kernel evaluated on a time-reflected test function. This follows directly from freeCovarianceℂ_bilinear_integrable since compTimeReflection maps test functions to test functions.

theorem compTimeReflection_toComplex_eq_ofReal (f : TestFunction) (x : SpaceTime) : (QFT.compTimeReflection (toComplex f)) x = ↑((QFT.compTimeReflectionReal f) x)

Relationship between compTimeReflection of toComplex and compTimeReflectionReal: they agree pointwise as complex values.

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

The real part of a complex integral of a real-valued function equals the real integral. This uses integral_ofReal_eq and Complex.ofReal_re.

theorem integrable_real_covariance_kernel (m : ℝ) [Fact (0 < m)] (f : TestFunction) : MeasureTheory.Integrable (fun (p : SpaceTime × SpaceTime) => (QFT.compTimeReflectionReal f) p.1 * freeCovariance m p.1 p.2 * f p.2) (MeasureTheory.volume.prod MeasureTheory.volume)

Integrability of the real covariance kernel obtained from a real test function.

theorem integral_prod_real_covariance_kernel (m : ℝ) [Fact (0 < m)] (f : TestFunction) : ∫ (p : SpaceTime × SpaceTime), (QFT.compTimeReflectionReal f) p.1 * freeCovariance m p.1 p.2 * f p.2 ∂MeasureTheory.volume.prod MeasureTheory.volume = ∫ (x : SpaceTime) (y : SpaceTime), (QFT.compTimeReflectionReal f) x * freeCovariance m x y * f y

Fubini helper: rewrite the real kernel double integral over the product measure.

theorem integral_prod_complex_covariance_kernel (m : ℝ) [Fact (0 < m)] (f : TestFunction) : ∫ (p : SpaceTime × SpaceTime), (QFT.compTimeReflection (toComplex f)) p.1 * ↑(freeCovariance m p.1 p.2) * (toComplex f) p.2 ∂MeasureTheory.volume.prod MeasureTheory.volume = ∫ (x : SpaceTime) (y : SpaceTime), (QFT.compTimeReflection (toComplex f)) x * ↑(freeCovariance m x y) * (toComplex f) y

Complex Fubini helper mirroring integral_prod_real_covariance_kernel.

theorem real_integral_eq_complex_re (m : ℝ) [Fact (0 < m)] (f : TestFunction) : ∫ (x : SpaceTime) (y : SpaceTime), (QFT.compTimeReflectionReal f) x * freeCovariance m x y * f y = (∫ (x : SpaceTime) (y : SpaceTime), (QFT.compTimeReflection (toComplex f)) x * ↑(freeCovariance m x y) * (toComplex f) y).re

** (Real-Complex Integral Correspondence):** The real integral with compTimeReflectionReal equals the real part of the corresponding complex integral after complexification.

Proof idea: The complex integrand equals (r x y : ℂ) where r is the real integrand (using compTimeReflection_toComplex_eq_ofReal and toComplex_apply). For real-valued integrands, the .re of the complex integral equals the real integral via integral_ofReal_eq applied twice.

theorem toComplex_star_eq (f : TestFunction) (x : SpaceTime) : (starRingEnd ℂ) ((toComplex f) x) = (toComplex f) x

** (Complex Conjugate Identity for Real Functions):** For real-valued test functions lifted to complex, the complex conjugate equals the original. This allows us to match the Parseval identity which uses starRingEnd.

theorem compTimeReflection_toComplex_star_eq (f : TestFunction) (x : SpaceTime) : (starRingEnd ℂ) ((QFT.compTimeReflection (toComplex f)) x) = (QFT.compTimeReflection (toComplex f)) x

The time-reflected complexification of a real test function remains real-valued.

Euclidean Invariance

theorem freeCovariance_euclidean_invariant (m : ℝ) (g : QFT.E) (x y : SpaceTime) : freeCovariance m (QFT.act g x) (QFT.act g y) = freeCovariance m x y

Euclidean invariance of the free covariance. Since freeCovariance only depends on ‖x - y‖ (via the Bessel form), and Euclidean transformations preserve distances, this follows immediately.

noncomputable def timeReflectionE : QFT.E

Time reflection as an element of the Euclidean group (rotation with no translation).

Equations

• timeReflectionE = { R := QFT.timeReflectionLE.toLinearIsometry, t := 0 }

theorem act_timeReflectionE (x : SpaceTime) : QFT.act timeReflectionE x = QFT.timeReflection x

The Euclidean action of timeReflectionE equals timeReflection.

theorem covariance_timeReflection_invariant (m : ℝ) (x y : SpaceTime) : freeCovariance m (QFT.timeReflection x) (QFT.timeReflection y) = freeCovariance m x y

** (Time Reflection Invariance - Position Space):** The position-space covariance kernel is invariant under geometric time reflection. This follows from general Euclidean invariance since time reflection is in O(4).

Complex Extension

Note: freeCovarianceℂBilinear is defined in Parseval.lean (imported above). The following lemmas prove properties of this bilinear form.

theorem freeCovarianceℂ_bilinear_inner_integrable (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : MeasureTheory.Integrable (fun (x : SpaceTime) => ∫ (y : SpaceTime), f x * ↑(freeCovariance m x y) * g y) MeasureTheory.volume

For each fixed x, the inner integral in the complex bilinear form is absolutely integrable. This follows from product integrability (freeCovarianceℂ_bilinear_integrable) plus Fubini.

theorem freeCovarianceℂ_bilinear_slice_integrable (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : ∀ᵐ (x : SpaceTime), MeasureTheory.Integrable (fun (y : SpaceTime) => f x * ↑(freeCovariance m x y) * g y) MeasureTheory.volume

For each fixed x, the inner integral defining the bilinear form is integrable in y. Together with the previous lemma, this allows iterated integration. Follows from product integrability via Fubini (Integrable.prod_right_ae).

theorem freeCovarianceℂ_bilinear_add_smul_left (m : ℝ) [Fact (0 < m)] (c : ℂ) (f₁ f₂ g : TestFunctionℂ) : freeCovarianceℂBilinear m (c • f₁ + f₂) g = c * freeCovarianceℂBilinear m f₁ g + freeCovarianceℂBilinear m f₂ g

Generalized bilinearity in the first argument: scalar multiplication and addition combined.

theorem freeCovarianceℂ_bilinear_add_left (m : ℝ) [Fact (0 < m)] (f₁ f₂ g : TestFunctionℂ) : freeCovarianceℂBilinear m (f₁ + f₂) g = freeCovarianceℂBilinear m f₁ g + freeCovarianceℂBilinear m f₂ g

theorem freeCovarianceℂ_bilinear_smul_left (m : ℝ) [Fact (0 < m)] (c : ℂ) (f g : TestFunctionℂ) : freeCovarianceℂBilinear m (c • f) g = c * freeCovarianceℂBilinear m f g

theorem freeCovarianceℂ_bilinear_symm (m : ℝ) [Fact (0 < m)] (f g : TestFunctionℂ) : freeCovarianceℂBilinear m f g = freeCovarianceℂBilinear m g f

Symmetry of the complex bilinear form: swapping arguments gives the same result.

theorem freeCovarianceℂ_bilinear_smul_right (m : ℝ) [Fact (0 < m)] (c : ℂ) (f g : TestFunctionℂ) : freeCovarianceℂBilinear m f (c • g) = c * freeCovarianceℂBilinear m f g

theorem freeCovarianceℂ_bilinear_add_right (m : ℝ) [Fact (0 < m)] (f g₁ g₂ : TestFunctionℂ) : freeCovarianceℂBilinear m f (g₁ + g₂) = freeCovarianceℂBilinear m f g₁ + freeCovarianceℂBilinear m f g₂

noncomputable def freeCovarianceℂRegulated (α m : ℝ) (f g : TestFunctionℂ) : ℂ

Complex extension of the covariance for complex test functions, using regulated Fourier form.

Equations

• freeCovarianceℂRegulated α m f g = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovarianceRegulated α m x y) * (starRingEnd ℂ) (g y)

theorem freeCovarianceℂ_regulated_positive (α : ℝ) (hα : 0 < α) (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : 0 ≤ (freeCovarianceℂRegulated α m f f).re

The regulated complex covariance is positive definite for any α > 0.

noncomputable def freeCovarianceℂ (m : ℝ) (f g : TestFunctionℂ) : ℂ

Complex extension of the covariance for complex test functions (limit form via Bessel).

Equations

• freeCovarianceℂ m f g = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovariance m x y) * (starRingEnd ℂ) (g y)

theorem freeCovarianceℂ_positive (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : 0 ≤ (freeCovarianceℂ m f f).re

The complex covariance (Bessel form) is positive definite.

theorem parseval_covariance_schwartz_bessel (m : ℝ) [Fact (0 < m)] (f : TestFunctionℂ) : (freeCovarianceℂ m f f).re = ∫ (k : SpaceTime), ‖((SchwartzMap.fourierTransformCLM ℂ) f) k‖ ^ 2 * freePropagatorMomentumMathlib m k

(Parseval for Bessel Covariance): The Parseval identity for the well-defined Bessel form of the covariance. This directly relates the position-space covariance integral to the momentum-space integral.

Note: Unlike the regulated form, this uses freeCovariance (Bessel K₁ form) which is well-defined pointwise. The equality holds because the Bessel form equals the limit of the regulated forms.

OS Properties