Parseval Identity for Covariance #
This file proves the fundamental Parseval identity relating the position-space covariance bilinear form to the momentum-space propagator.
Statement #
For a Schwartz test function f : TestFunctionℂ and mass m > 0:
(∫∫ f(x) * C(x,y) * conj(f(y)) dx dy).re = ∫ |f̂(k)|² * P(k) dk
where:
- C(x,y) = freeCovariance m x y is the position-space propagator
- P(k) = freePropagatorMomentum m k = 1/(‖k‖² + m²) is the momentum-space propagator
- f̂ = SchwartzMap.fourierTransformCLM ℂ f is the Fourier transform
Proof Strategy #
Substitute Fourier representation of C(x,y): C(x,y) = (∫ P(k) e^{-ik·(x-y)} dk / (2π)^d).re
Apply Fubini to swap integrals (integrate over x and y first): ∫∫∫ f(x) * P(k) * e^{-ik·(x-y)} * conj(f(y)) dx dy dk
Recognize Fourier transforms:
- ∫ f(x) e^{-ikx} dx relates to f̂(k)
- ∫ conj(f(y)) e^{iky} dy relates to conj(f̂(k))
Handle normalization mismatch:
- Physics convention: exp(-i k·x) with (2π)^d normalization
- Mathlib convention: exp(-2πi ⟨v,w⟩) (unitary normalization)
Combine to get |f̂(k)|² * P(k)
Main Difficulties #
- Normalization: Physics uses exp(-ik·x)/(2π)^d, Mathlib uses exp(-2πi⟨x,k⟩)
- Multiple integrability conditions need verification
- Fubini requires showing the triple integral is absolutely convergent
Normalization constant for the Fourier transform.
Equations
- fourierNormalization d = (2 * Real.pi) ^ d
Instances For
Bridge Lemmas #
These lemmas connect the physics-convention Fourier transform (used in freeCovariance) to Mathlib's convention (used in SchwartzMap.fourierTransformCLM).
Fourier Transform Convention Analysis #
IMPORTANT: There is a convention mismatch between physics and Mathlib Fourier transforms.
Mathlib convention (from Real.fourierIntegral_eq):
𝓕 f(k) = ∫ f(x) exp(-2πi⟨x, k⟩) dx
Physics convention (used in freeCovariance):
f̂_phys(k) = ∫ f(x) exp(-i⟨k, x⟩) dx
Relationship:
f̂_phys(k) = 𝓕 f(k/(2π))
This means:
|f̂_phys(k)|² = |𝓕 f(k/(2π))|² (evaluated at DIFFERENT momenta)
NOT:
|f̂_phys(k)|² = (2π)^d |𝓕 f(k)|² (this is FALSE for generic f)
Impact on Parseval identity:
After Fubini, the LHS becomes:
(1/(2π)^d) ∫_k P(k) |f̂_phys(k)|² dk
With change of variables p = k/(2π):
= ∫_p P(2πp) |𝓕 f(p)|² dp
= ∫_p |𝓕 f(p)|² / (4π²‖p‖² + m²) dp
So the correct Parseval identity using Mathlib's FT should have propagator 1/(4π²‖p‖² + m²),
NOT 1/(‖p‖² + m²).
The lemma parseval_covariance_schwartz now correctly uses
freePropagatorMomentumMathlib m k = 1/((2π)²‖k‖² + m²) with Mathlib's fourierTransformCLM.
The relationship between physics and Mathlib propagators under rescaling.
freePropagatorMomentumMathlib is defined in Covariance.Momentum.
The scaling factor for momentum integration change of variables.
Equations
Instances For
The scaling map on momentum space: k ↦ 2πk
Equations
Instances For
The momentum scaling as a linear equivalence.
Equations
Instances For
Physics vs Mathlib Fourier Transform Bridge #
The "physics" Fourier transform uses convention ∫ f(x) exp(-i⟨k,x⟩) dx
while Mathlib uses ∫ f(x) exp(-2πi⟨x,ξ⟩) dx.
Key relationship: f̂_phys(2πξ) = 𝓕f(ξ)
The physics-convention Fourier transform of a Schwartz function.
Uses exp(-i⟨k,x⟩) instead of Mathlib's exp(-2πi⟨x,ξ⟩).
Equations
Instances For
The regulated Fourier covariance equals the full complex Fourier integral, not just the real part. The regulator exp(-α‖k‖²) ensures absolute convergence.
Regulated Parseval Identity - Full Proof #
The following section contains the complete proof of the regulated Parseval identity, The proof uses:
- Gaussian regulator for absolute convergence
- Fubini theorem for integral reordering
- Phase factorization for separating x and y integrals
- Change of variables from physics to Mathlib Fourier convention
The free propagator is bounded by 1/m².
The free propagator is strictly positive.
The Gaussian regulator exp(-α‖k‖²) is integrable for α > 0.
The norm of the regulated propagator as a complex number.
The inner product function is measurable.
The phase exponential exp(-i⟨k,x⟩) is measurable.
The conjugate phase exponential exp(i⟨k,x⟩) is measurable.
A Schwartz function times the phase exp(-i⟨k,x⟩) is integrable.
The conjugate of a Schwartz function times the phase exp(i⟨k,y⟩) is integrable.
The bounding function for the triple integrand is integrable.
The triple integrand is bounded by the integrable bounding function.
The regulated integrand is integrable in all variables jointly.
The physics FT at 2πξ equals the Mathlib FT at ξ.
The integrand transforms correctly under k = 2π•p.
After Fubini, the inner k-integral factorizes.
The y-integral with conjugate equals the conjugate of the physics FT.
The product physicsFT f k * conj(physicsFT f k) = ‖physicsFT f k‖²
The factorized form simplifies to an integral of |physics FT|².
Parseval identity for regulated covariance (proven theorem).
This is the fundamental identity relating the position-space covariance integral to the momentum-space integral. The regulator exp(-α‖k‖²) ensures absolute convergence.
The proof proceeds by:
- Expanding freeCovarianceRegulated as a Fourier integral
- Applying Fubini (justified by regulated_triple_integrable)
- Factoring the phase using phase_factorization
- Recognizing the x and y integrals as Fourier transforms
- Accounting for normalization factors via change of variables
Continuity of the mathlib propagator.
The integrand ‖f̂(k)‖² * P(k) is integrable for Schwartz f.
The unregulated Parseval identity as a limit. This theorem explicitly shows that the regulated covariance integral converges to the unregulated momentum-space integral as α → 0⁺.
The proof uses dominated convergence to pass from the regulated identity (parseval_covariance_schwartz_regulated) to the unregulated limit.
Complex bilinear form convergence (general f, g): The regulated bilinear covariance form converges to the Bessel form as α → 0⁺ for arbitrary complex test functions f, g.
Proof outline: Dominated convergence theorem on the product space:
- Pointwise convergence:
freeCovariance_regulated_limit_eq_freeCovariance - Dominator: exp(m²) × |f(x)| × |C_Bessel(x,y)| × |g(y)| is integrable
- Bound:
freeCovariance_regulated_le_const_mul_freeCovariancegives the uniform bound
Complex convergence for the symmetric case (f = f): The regulated bilinear form converges to the Bessel form in ℂ when both test functions are the same.
This is a direct corollary of bilinear_covariance_regulated_tendstoℂ with g = f.
Global Definitions #
The following definitions are placed outside the section to ensure they are accessible globally without namespace qualification.
Bilinear extension of the covariance for complex test functions. This is the distributional formulation: the double integral is well-defined for Schwartz test functions due to the L¹ integrability of the Bessel kernel.
Equations
- freeCovarianceℂBilinear m f g = ∫ (x : SpaceTime) (y : SpaceTime), f x * ↑(freeCovariance m x y) * g y