Real Covariance Form and Square Root Propagator Embedding

This file provides the real covariance form infrastructure along with the proof of the square root propagator embedding theorem.

Main Results

• freeCovarianceFormR: The real covariance bilinear form
• sqrtPropagatorEmbedding: Existence of linear embedding realizing covariance as squared norm
• freeCovarianceFormR_continuous: Continuity of the quadratic form f ↦ C(f,f)
• freeCovarianceFormR_pos: Positivity of the quadratic form

Real Covariance Form

noncomputable def QFT.freeCovarianceFormR (m : ℝ) (f g : TestFunction) : ℝ

Real covariance bilinear form induced by the free covariance kernel.

Equations

• QFT.freeCovarianceFormR m f g = ∫ (x : SpaceTime) (y : SpaceTime), f x * freeCovariance m x y * g y

theorem QFT.freeCovarianceℂ_bilinear_agrees_on_reals (m : ℝ) (f g : TestFunction) : freeCovarianceℂBilinear m (toComplex f) (toComplex g) = ↑(freeCovarianceFormR m f g)

Weighted L² Space Construction

noncomputable def QFT.momentumWeightMeasure (m : ℝ) : MeasureTheory.Measure SpaceTime

The weighted measure on momentum space with density (‖k‖² + m²)⁻¹.

Equations

• QFT.momentumWeightMeasure m = MeasureTheory.volume.withDensity fun (k : SpaceTime) => ENNReal.ofReal (momentumWeight m k)

noncomputable def QFT.fourierTransformCLMReal : TestFunctionℂ →L[ℝ] TestFunctionℂ

ℝ-linear view of the complex Fourier transform on Schwartz space.

Note: we build this manually instead of using restrictScalars because the LinearMap.CompatibleSMul instance is not found automatically in mathlib v4.29.

Equations

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

noncomputable def QFT.schwartzToL2CLMReal (_m : ℝ) : TestFunctionℂ →L[ℝ] ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

ℝ-linear view of the Schwartz-to-L² embedding.

Equations

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

The Embedding Map

noncomputable def QFT.sqrtPropagatorMap (m : ℝ) (f : TestFunction) : SpaceTime → ℂ

The embedding T maps a test function to a weighted function in momentum space. Conceptually: T f = FourierTransform(f) * (‖k‖² + m²)^(-1/2).

Equations

• QFT.sqrtPropagatorMap m f k = ((SchwartzMap.fourierTransformCLM ℂ) (toComplex f)) k * ↑(momentumWeightSqrtMathlib m k)

theorem QFT.sqrtPropagatorMap_sq_integrable (m : ℝ) [Fact (0 < m)] (f : TestFunction) : MeasureTheory.Integrable (fun (k : SpaceTime) => ‖sqrtPropagatorMap m f k‖ ^ 2) MeasureTheory.volume

The sqrtPropagatorMap is square-integrable.

theorem QFT.sqrtPropagatorMap_memLp (m : ℝ) [Fact (0 < m)] (f : TestFunction) : MeasureTheory.MemLp (sqrtPropagatorMap m f) 2 MeasureTheory.volume

The weighted Fourier representative lies in L².

noncomputable def QFT.sqrtPropagatorMapNormSq (m : ℝ) (f : TestFunction) : ℝ

The squared L² norm of the mapped function.

Equations

• QFT.sqrtPropagatorMapNormSq m f = ∫ (k : SpaceTime), ‖QFT.sqrtPropagatorMap m f k‖ ^ 2

theorem QFT.sqrtPropagatorMap_linear_add (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : sqrtPropagatorMap m (f + g) = sqrtPropagatorMap m f + sqrtPropagatorMap m g

The map is linear in f (additive).

theorem QFT.sqrtPropagatorMap_linear_smul (m : ℝ) [Fact (0 < m)] (c : ℝ) (f : TestFunction) : sqrtPropagatorMap m (c • f) = c • sqrtPropagatorMap m f

The map is ℝ-linear (scalar multiplication).

Connection to Covariance

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

For real test functions, the star (conjugation) of toComplex is the identity.

theorem QFT.freeCovarianceℂ_eq_bilinear_on_reals (m : ℝ) (f g : TestFunction) : freeCovarianceℂ m (toComplex f) (toComplex g) = freeCovarianceℂBilinear m (toComplex f) (toComplex g)

For real test functions, freeCovarianceℂ agrees with freeCovarianceℂBilinear.

theorem QFT.sqrtPropagatorMap_norm_eq_covariance (m : ℝ) [Fact (0 < m)] (f : TestFunction) : sqrtPropagatorMapNormSq m f = freeCovarianceFormR m f f

Key lemma: The squared norm equals the covariance form.

The Proof of sqrtPropagatorEmbedding

@[reducible, inline]

abbrev QFT.TargetHilbertSpace (_m : ℝ) : Type

The target Hilbert space: L²(SpaceTime, Lebesgue) with complex values.

Equations

• QFT.TargetHilbertSpace _m = ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

noncomputable def QFT.embeddingMap (m : ℝ) [Fact (0 < m)] : TestFunction →ₗ[ℝ] TargetHilbertSpace m

The linear map T: TestFunction → L².

Equations

• QFT.embeddingMap m = { toFun := fun (f : TestFunction) => MeasureTheory.MemLp.toLp (QFT.sqrtPropagatorMap m f) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem QFT.embeddingMap_norm_sq (m : ℝ) [Fact (0 < m)] (f : TestFunction) : ‖(embeddingMap m) f‖ ^ 2 = ∫ (k : SpaceTime), ‖sqrtPropagatorMap m f k‖ ^ 2

Squared L² norm of the embedded function in terms of the pointwise integral.

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

Continuous linear map obtained by composing the proven building blocks.

Equations

• QFT.embeddingMapCLM m = (QFT.momentumWeightSqrt_mathlib_mul_CLM_real✝ m ∘SL QFT.schwartzToL2CLMReal m) ∘SL QFT.fourierTransformCLMReal ∘SL toComplexCLM

theorem QFT.embeddingMapCLM_apply (m : ℝ) [Fact (0 < m)] (f : TestFunction) : (embeddingMapCLM m) f = (embeddingMap m) f

theorem QFT.sqrtPropagatorEmbedding (m : ℝ) [Fact (0 < m)] : ∃ (H : Type) (x : NormedAddCommGroup H) (x_1 : InnerProductSpace ℝ H) (T : TestFunction →ₗ[ℝ] H), ∀ (f : TestFunction), freeCovarianceFormR m f f = ‖T f‖ ^ 2

Existence of a linear embedding realizing the free covariance as a squared norm. The target space H is an inner product space (L² is a Hilbert space). Note: InnerProductSpace ℝ H implies NormedSpace ℝ H via InnerProductSpace.toNormedSpace.

Auxiliary Lemmas for Continuity

theorem QFT.freeCovarianceFormR_eq_normSq (m : ℝ) [Fact (0 < m)] (f : TestFunction) : freeCovarianceFormR m f f = ‖(embeddingMap m) f‖ ^ 2

theorem QFT.embeddingMap_continuous (m : ℝ) [Fact (0 < m)] : Continuous ⇑(embeddingMap m)

The embedding map TestFunction → L² is continuous.

theorem QFT.freeCovarianceFormR_continuous (m : ℝ) [Fact (0 < m)] : Continuous fun (f : TestFunction) => freeCovarianceFormR m f f

Continuity of the real covariance quadratic form f ↦ C(f,f).

Positivity and Other Properties

theorem QFT.freeCovarianceFormR_pos (m : ℝ) [Fact (0 < m)] (f : TestFunction) : 0 ≤ freeCovarianceFormR m f f

Positivity of the real covariance quadratic form.

theorem QFT.freeCovarianceFormR_symm (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : freeCovarianceFormR m f g = freeCovarianceFormR m g f

Symmetry of the real covariance bilinear form.

theorem QFT.freeCovarianceFormR_add_left (m : ℝ) [Fact (0 < m)] (f₁ f₂ g : TestFunction) : freeCovarianceFormR m (f₁ + f₂) g = freeCovarianceFormR m f₁ g + freeCovarianceFormR m f₂ g

Linearity in the first argument of the real covariance bilinear form.

theorem QFT.freeCovarianceFormR_smul_left (m : ℝ) [Fact (0 < m)] (c : ℝ) (f g : TestFunction) : freeCovarianceFormR m (c • f) g = c * freeCovarianceFormR m f g

Scalar multiplication in the first argument of the real covariance bilinear form.

theorem QFT.freeCovarianceFormR_add_right (m : ℝ) [Fact (0 < m)] (f g₁ g₂ : TestFunction) : freeCovarianceFormR m f (g₁ + g₂) = freeCovarianceFormR m f g₁ + freeCovarianceFormR m f g₂

Addition in the second argument of the real covariance bilinear form.

theorem QFT.freeCovarianceFormR_smul_right (m : ℝ) [Fact (0 < m)] (c : ℝ) (f g : TestFunction) : freeCovarianceFormR m f (c • g) = c * freeCovarianceFormR m f g

Scalar multiplication in the second argument of the real covariance bilinear form.

theorem QFT.freeCovarianceFormR_zero_left (m : ℝ) [Fact (0 < m)] (g : TestFunction) : freeCovarianceFormR m 0 g = 0

Zero in the first argument gives zero.

theorem QFT.freeCovarianceFormR_zero_right (m : ℝ) [Fact (0 < m)] (f : TestFunction) : freeCovarianceFormR m f 0 = 0

Zero in the second argument gives zero.

theorem QFT.freeCovarianceFormR_reflection_invariant (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : freeCovarianceFormR m (compTimeReflectionReal f) (compTimeReflectionReal g) = freeCovarianceFormR m f g

theorem QFT.freeCovarianceFormR_reflection_cross (m : ℝ) [Fact (0 < m)] (f g : TestFunction) : freeCovarianceFormR m (compTimeReflectionReal f) g = freeCovarianceFormR m (compTimeReflectionReal g) f

Mixed-time-reflection identity for the real free covariance.

theorem QFT.freeCovarianceFormR_left_linear_any_right (m : ℝ) [Fact (0 < m)] {n : ℕ} (f : Fin n → PositiveTimeTestFunction) (c : Fin n → ℝ) (s : Finset (Fin n)) (g : TestFunction) : ∑ i ∈ s, c i * freeCovarianceFormR m (compTimeReflectionReal ↑(f i)) g = freeCovarianceFormR m (∑ i ∈ s, c i • compTimeReflectionReal ↑(f i)) g

Left linearity of freeCovarianceFormR for any fixed right argument.