OS3 — Mixed Representation via Schwinger Parametrization #
Derives the mixed (momentum-position) representation of the covariance bilinear form
by performing the Fubini exchanges justified in OS3_MixedRepInfra. The chain is:
- Schwinger → heat kernel: ⟨Θf, Cf⟩ = ∫₀^∞ e^{−sm²} [∫∫ f*(x) f(y) H(s,|Θx−y|)] ds
- Fourier representation of heat kernel introduces spatial momenta kbar
- k₀ Gaussian integral: ∫ e^{ik₀(x₀+y₀)} e^{−sk₀²} dk₀ = √(π/s) e^{−(x₀+y₀)²/4s}
- Laplace transform in s: ∫₀^∞ s^{−1/2} e^{−(x₀+y₀)²/4s − sω²} ds = √(π/ω²) e^{−ω|x₀+y₀|}
The final result (Bessel K_{1/2} identity) is:
⟨Θf, Cf⟩ = (1/2(2π)³) ∫_{kbar} ∫∫ f*(x) f(y) (1/ω) e^{−ω|x₀+y₀|} e^{ikbar·(xbar−ybar)} dkbar dx dy
This is the integration order exchange from eq. (4.19) that the naive approach could not justify due to the non-absolute-integrability of 1/√(k²+m²) in 3D.
- Fubini Theorems (from
OS3_MixedRepInfra): Justify all changes in integration order using the integrability bounds.
Physical Interpretation #
The mixed representation exhibits:
- Causality: Exponential decay
e^(-ω|x⁰+y⁰|)forx⁰,y⁰ ≤ 0(reflection positivity support). - On-shell condition: The energy-momentum relation
ω² = |k|² + m²is built into the structure. - Feynman propagator: The k⁰ integral has poles at ±iω, corresponding to particle propagation.
References #
- Osterwalder & Schrader, "Axioms for Euclidean Green's Functions I & II" (1973, 1975)
- Glimm & Jaffe, "Quantum Physics: A Functional Integral Point of View" (1987), §11.4
- Haag, "Local Quantum Physics" (1996), §V.3
The 1D Gaussian Fourier transform in real form: ∫ exp(-ik₀t) exp(-sk₀²) dk₀ = √(π/s) exp(-t²/(4s))
This follows from Mathlib's fourierIntegral_gaussian.
Gaussian exponential factorizes: exp(-s‖k‖²) = exp(-sk₀²) × exp(-s‖k_sp‖²)
The k₀-integral evaluates to √(π/s) exp(-t²/(4s)) times the k_sp-dependent factor.
For z = Θx - y with z₀ = -x₀ - y₀: ∫k exp(-ik·z) exp(-s|k|²) = (∫{k₀} exp(-ik₀z₀) exp(-sk₀²)) × (∫{k_sp} exp(-ik_sp·z_sp) exp(-s|k_sp|²)) = √(π/s) exp(-z₀²/(4s)) × ∫{k_sp} exp(-ik_sp·z_sp) exp(-s|k_sp|²)
The spatial part of (timeReflection x - y) equals spatialPart x - spatialPart y.
THEOREM: Heat kernel bilinear form after k₀ integration.
Starting from the Schwinger representation with heat kernel H(s,r):
∫₀^∞ exp(-sm²) ∫∫ fbar(x)f(y) H(s, |Θx-y|) dx dy ds
After substituting H(s,r) = (2π)^{-d} ∫_k exp(-ik·z) exp(-s|k|²) and performing the k₀ integral using the 1D Gaussian FT:
∫_{-∞}^∞ exp(-ik₀t) exp(-sk₀²) dk₀ = √(π/s) · exp(-t²/(4s))
we obtain:
(2π)^{-4} ∫₀^∞ ∫_pbar ∫∫ fbar(x)f(y) √(π/s) exp(-t²/(4s)) exp(-s(|pbar|² + m²)) exp(-ipbar·rbar) dx dy d³pbar ds
where t = -x₀ - y₀ (time separation under reflection) and rbar = xbar - ybar (spatial separation).
The exp(-sm²) factor combines with exp(-s|pbar|²) to give exp(-s(|pbar|² + m²)).
Helper lemmas for Laplace s-integral evaluation #
The s-integral evaluation for fixed (k_sp, x, y):
∫_s √(π/s) exp(-t²/(4s)) exp(-s·ω²) ds = (π/ω) exp(-ω|t|)
where t = -(x₀) - y₀ and ω = √(‖k_sp‖² + m²).
This uses laplace_integral_half_power_nonneg from LaplaceIntegral.lean.
Proof outline:
- Factor √(π/s) = √π · s^(-1/2)
- Combine exponentials: exp(-t²/(4s)) * exp(-sω²) = exp(-t²/(4s) - sω²)
- Apply laplace_integral_half_power_nonneg with a = t²/4, b = ω²
- Result: √π * √(π/ω²) * exp(-2√((t²/4)*ω²)) = (π/ω) * exp(-ω|t|)
Complex version of s_integral_eval: The Laplace integral identity in ℂ.
This is a direct corollary of s_integral_eval, converting the real integral
to complex form. The key observation is that all terms in the integrand are
real numbers cast to ℂ, so we can use integral_ofReal to relate the integrals.
∫_s (↑√(π/s)) * cexp(-↑(t²/(4s))) * cexp(-↑(sω²)) ds = ↑((π/ω) * exp(-ω|t|))
Complex-valued s-integral: For fixed (k_sp, x, y, f), the inner s-integral with complex exponentials evaluates to the propagator form.
This wraps s_integral_eval by:
- Factoring out constant terms (fbarf and phase)
- Converting Complex.exp to Real.exp for real arguments
- Applying s_integral_eval
- Reassembling the complex result
Note: The integrand has the form: fbar * f * √(π/s) * cexp(-t²/(4s)) * cexp(-sω²) * cexp(-I*phase)
where all exponentials have real arguments (cast to ℂ).
THEOREM: Laplace transform evaluation for the s-integral.
The key identity (Bessel K_{1/2} / modified Laplace transform):
√π · ∫₀^∞ s^{-1/2} exp(-t²/(4s) - sω²) ds = (π/ω) · exp(-ω|t|)
where ω = √(|pbar|² + m²) is the relativistic dispersion relation.
This transforms the Schwinger proper-time representation into the Euclidean propagator in mixed (pbar, x₀) representation:
1/(2π)⁴ · ∫_pbar ∫₀^∞ √(π/s) exp(-t²/(4s)) exp(-s(|pbar|² + m²)) exp(-ipbar·rbar) ds d³pbar = 1/(2(2π)³) · ∫_pbar (1/ω) exp(-ω|t|) exp(-ipbar·rbar) d³pbar
Normalization: (1/(2π)⁴) × π = 1/(2(2π)³) ✓
Proof: Uses fubini_s_xy_swap to move s inside, then
s_integral_eval to evaluate the Laplace transform.
THEOREM: The triple product (s, x, y) of the Schwinger-heat kernel bilinear form is integrable.
This allows applying Fubini to swap ∫_s with ∫_x ∫_y.
Proof:
Uses Integrable.mono' with the bound from schwinger_bound_integrable.
The pointwise bound |integrand| ≤ bound is verified for s > 0,
and the set s ≤ 0 has measure zero under the restricted measure.
Fubini swap for the Schwinger integrand.
Given integrability of the Schwinger integrand on the product space, the iterated integrals can be computed in either order: ∫_x ∫_y ∫_s F = ∫_s ∫_x ∫_y F
Proof:
Both sides equal ∫∫∫ F over (Ioi 0) × SpaceTime × SpaceTime by Fubini-Tonelli.
The proof uses integral_prod to convert iterated integrals to product integrals,
and the measure-preserving map schwinger_tripleReorder to connect them.
Triple integral order swap.
Given integrability (from schwinger_bilinear_integrable), Fubini's theorem ensures:
∫ x ∫ y, F(x,y) * [∫ s, G(s,x,y)] = ∫ s, [∫ x ∫ y, F(x,y) * G(s,x,y)]
Proof sketch:
This follows from Mathlib's MeasureTheory.integral_integral_swap (Fubini-Tonelli)
applied to the integrable function from schwinger_bilinear_integrable.
The key steps:
- Rewrite both sides as integrals over ℝ × SpaceTime × SpaceTime
- Apply Fubini to swap the order of integration
- Use the integrability hypothesis to justify the swap
The kernel-level Schwinger representation holds for Θx ≠ y.
This follows from covarianceSchwingerRep_eq_freeCovarianceBessel.
Bessel bilinear form equals the Schwinger heat kernel form.
This follows from:
Kernel equality (a.e.): For Θx ≠ y (which is a.e. in the product measure), freeCovariance(Θx, y) = covarianceSchwingerRep(|Θx - y|) = ∫₀^∞ e^{-sm²} H(s, |Θx-y|) ds This is proven via
covarianceSchwingerRep_eq_freeCovarianceBessel.Fubini swap: Exchanging the s-integral with the x,y-integrals. Uses
schwinger_bilinear_integrable.
Mathematical statement: ∫∫ conj(f(x)) C(Θx,y) f(y) dx dy = ∫₀^∞ e^{-sm²} [∫∫ conj(f) f H(s,|Θx-y|) dx dy] ds
Heat kernel bilinear form equals the mixed representation.
This encapsulates the multi-step transformation from heat kernel to mixed rep:
- Apply
heatKernel_eq_gaussianFT: H(s,r) = (1/(2π)^d) ∫_k exp(-ik·z) exp(-s|k|²) - Decompose k = (k₀, k_sp) into time and spatial momenta
- Do k₀ integral using
gaussian_fourier_1d: gives √(π/s) exp(-t²/(4s)) - Fubini swap: exchange s and k_sp integrals (justified by Schwartz decay)
- Do s-integral using
laplace_integral_half_powerwith a = t²/4, b = |k_sp|² + m²: √π ∫₀^∞ s^{-1/2} exp(-t²/(4s) - (|k_sp|²+m²)s) ds = (π/ω) exp(-ω|t|) - Normalize: (1/(2π)^4) × π = 1/(2(2π)³)
Dependencies:
heatKernel_eq_gaussianFT(PROVEN, line 153)gaussian_fourier_1d(PROVEN, line 814)laplace_integral_half_power(THEOREM, line 135)- Fubini applications (require integrability - uses Schwartz decay)
THEOREM: The Bessel bilinear form equals the mixed representation form.
This connects the position-space Bessel kernel to its momentum-space mixed representation (spatial in momentum, time in position).
∫∫ conj(f(x)) C(Θx, y) f(y) dx dy = (1/(2(2π)^{d-1})) ∫_{k_sp} ∫_x ∫_y conj(f) f (1/ω) exp(-ω|t|) exp(-i k_sp·r_sp)
where ω = √(|k_sp|² + m²), t = -x₀ - y₀, r_sp = x_sp - y_sp.
Proof outline (directly at bilinear level):
Schwinger representation: Insert C(Θx,y) = ∫₀^∞ exp(-sm²) H(s,|Θx-y|) ds
Heat kernel as Gaussian FT: By
heatKernel_eq_gaussianFT, H(s,r) = (1/(2π)^d) ∫_k exp(-ik·z) exp(-s|k|²) d^d kDecompose k = (k₀, k_sp): The 4D k-integral becomes product of 1D and 3D integrals
Do k₀ integral: By
gaussian_fourier_1d(PROVEN), ∫ exp(-ik₀t) exp(-sk₀²) dk₀ = √(π/s) exp(-t²/(4s))Fubini to swap s and k_sp: Justified by Schwartz decay of f (absolute convergence)
Do s-integral: By
laplace_integral_half_power(THEOREM) with a = t²/4, b = ω²: √π · ∫₀^∞ s^{-1/2} exp(-t²/(4s) - ω²s) ds = (π/ω) exp(-ω|t|)Normalize: (1/(2π)^4) × π = 1/(2(2π)³) ✓
Note: Working directly at bilinear level ensures absolute convergence (Schwartz test functions provide decay even when t = 0).
The mixed representation integrand can be converted to the k₀-inside form using the Fourier inversion identity for the Lorentzian.
By fourier_lorentzian_1d_neg:
(π/ω) exp(-ω|t|) = ∫_{k₀} exp(-ik₀t)/(k₀²+ω²) dk₀
So: (1/ω) exp(-ω|t|) = (1/π) ∫_{k₀} exp(-ik₀t)/(k₀²+ω²) dk₀
Bessel covariance bilinear form equals the k₀-inside momentum form.
This follows from:
bessel_bilinear_eq_mixed_representation: Bessel = mixed repmixed_rep_to_k0_inside_integrand: mixed rep integrand = k₀-inside integrand
The conversion between normalizations works out because:
- Mixed rep has factor: 1/(2(2π)^{d-1})
- Converting (1/ω) to (1/π)∫... multiplies by (1/π)
- Combined: 1/(2π(2π)^{d-1}) = 1/(2π)^d ✓
Proof sketch:
- Apply
bessel_bilinear_eq_mixed_representationto convert LHS to mixed rep - Use
mixed_rep_to_k0_inside_integrand: (1/ω) exp(-ω|t|) = (1/π) ∫_{k₀}... - Factor the spatial phase into the k₀ integral
- Combine normalizations: 1/(2(2π)^{d-1}) × (1/π) = 1/(2π)^d