OS3 Infrastructure — Schwinger Parametrization and Fubini Theorems #
The naive Fourier representation of covariance reflection positivity requires exchanging the k₀ integral with the x,y integrals, but the integrand 1/√(k²+m²) is NOT absolutely integrable in 3D k-space. The Schwinger parametrization resolves this:
⟨Θf, Cf⟩ = ∫₀^∞ e^{−sm²} [∫_x ∫_y f*(x) f(y) H(s, |Θx−y|)] ds
where H(s,r) = (4πs)^{−2} exp(−r²/4s) is the heat kernel, bounded by s^{−2}. The integrand is absolutely integrable: Schwartz functions are bounded, H is bounded, and e^{−sm²} provides exponential decay in s.
This file proves the Fubini theorems justifying integration order exchanges between proper-time s, spatial momenta k_sp, and spacetime points x,y. The integrability bounds use |f(x)||f(y)| ≤ C · x₀y₀ / (1+|xbar|²)^N(1+|ybar|²)^N for positive-time test functions, combined with Gaussian moment formulas for the time integrals.
Core Definitions #
Inner product on spatial coordinates: k_spatial · x_spatial = Σᵢ kᵢ xᵢ
Equations
- spatialDot k_spatial x_spatial = ∑ i : Fin (STDimension - 1), k_spatial.ofLp i * x_spatial.ofLp i
Instances For
spatialDot equals the real inner product on SpatialCoords.
Shared norm facts for the Fubini integrand factors #
The reflection-positivity Fubini integrand is a product of six factors. The following private lemmas record the norm of each factor; they are reused across the Fubini integrability and swap proofs below.
The inner product on SpaceTime decomposes into time and spatial parts: ⟪k, z⟫ = k₀ z₀ + ⟪k_sp, z_sp⟫ = k₀ z₀ + spatialDot(k_sp, z_sp)
Integral Decomposition for SpaceTime #
Auxiliary: The weighted Laplace-Fourier transform appearing in reflection positivity. F_ω(k_spatial) = ∫ dx f(x) exp(-|x₀| ω(k)) exp(i k_spatial · x_spatial)
This is the key quantity that appears after contour integration. For functions supported on positive time (x₀ ≥ 0), this becomes a product of two Fourier-Laplace transforms, leading to the squared norm factorization.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Time Reflection Properties #
Time reflection is measure-preserving (it's a linear isometry).
Time reflection is an involution: Θ(Θx) = x
Mixed Representation and k₀-inside Form #
The key step in the reflection positivity proof is to convert the Bessel bilinear form to a momentum representation where the k₀ integral is innermost.
Important mathematical point: The naive d⁴k momentum integral does NOT converge as a Lebesgue integral (it decays like 1/k² which is not integrable in 4D). The correct procedure uses the "mixed representation" of the Bessel kernel:
C(x,y) = (1/(2(2π)^{d-1})) ∫_{k_sp} (1/ω) exp(-ω|x₀-y₀|) exp(-i k_sp·(x_sp-y_sp))
This mixed form has:
- Time dependence in position space: exp(-ω|t|) (exponential decay)
- Spatial dependence in momentum space: exp(-i k_sp·r_sp)
The crucial observation is that by fourier_lorentzian_1d_neg:
(π/ω) exp(-ω|t|) = ∫_{k₀} exp(-ik₀t)/(k₀²+ω²) dk₀
So (1/ω) exp(-ω|t|) = (1/π) ∫_{k₀} exp(-ik₀t)/(k₀²+ω²) dk₀
This allows us to convert between:
- Mixed representation: with exp(-ω|t|) evaluated
- k₀-inside form: with ∫_{k₀} 1/(k₀²+ω²) unevaluated
Laplace Integral Identity #
The key mathematical identity underlying the mixed representation is:
∫₀^∞ s^{-1/2} exp(-a/s - bs) ds = √(π/b) exp(-2√(ab)) for a, b > 0
This is a standard result (modified Bessel K_{1/2}) that appears when computing the spatial Fourier transform of the heat kernel integrated against proper time.
Derivation sketch: The substitution u = √(a/b) exp(t) transforms this into an integral related to K_{1/2}. Since K_{1/2}(z) = √(π/(2z)) exp(-z), the identity follows.
d-dimensional Gaussian Fourier transform.
For d = 4, this states: (1/(2π)^4) ∫_{ℝ^4} exp(-ik·z) exp(-s|k|²) d⁴k = (4πs)^{-2} exp(-|z|²/(4s))
which equals heatKernelPositionSpace s |z|.
Proof:
Uses Mathlib's integral_cexp_neg_mul_sq_norm_add with b = s, c = -I, w = z:
∫ k, exp(-s‖k‖² + (-I)⟪z,k⟫) = (π/s)^{d/2} * exp((-I)²‖z‖²/(4s))
= (π/s)^{d/2} * exp(-‖z‖²/(4s))
Combined with the normalization (1/(2π)^d) and the heat kernel formula: (1/(2π)^d) * (π/s)^{d/2} = (4πs)^{-d/2}
Technical Integration Lemmas #
The following lemmas establish integrability and measurability conditions that are mathematically standard but require substantial Mathlib plumbing.
The heat kernel is jointly continuous on (0, ∞) × ℝ as a function of (t, r).
Heat kernel composition is AEStronglyMeasurable.
The function p ↦ heatKernelPositionSpace p.1 ‖timeReflection p.2.1 - p.2.2‖
is AEStronglyMeasurable with respect to the restricted product measure
(volume.restrict (Set.Ioi 0)).prod (volume.prod volume).
Real-valued version of heatKernelPositionSpace_aestronglyMeasurable.
The heat kernel integral is translation invariant: ∫_y H(s, ‖a - y‖) dy = ∫_z H(s, ‖z‖) dz = 1 for any a ∈ SpaceTime.
This follows from:
- Lebesgue measure on SpaceTime is translation invariant
- The norm satisfies ‖a - y‖ = ‖-(y - a)‖ = ‖y - a‖
- The heat kernel integrates to 1 (heatKernelPositionSpace_integral_eq_one)
The translated heat kernel is integrable (since its integral equals 1).
Nonnegativity of the Schwinger bound integrand (fixed s > 0).
Integrability in y of the Schwinger bound integrand for fixed s > 0, x.
Evaluate the y-integral of the Schwinger bound integrand for fixed s > 0, x.
Integrability in x of the Schwinger bound integrand (after integrating in y).
Integrability of the Schwinger bound integrand on (x,y) for fixed s > 0.
Compute the (x,y)-integral of the Schwinger bound integrand for fixed s > 0.
Fubini/Tonelli step for Schwinger bound integrability.
Bound function for Schwinger integrability is integrable.
For any Schwartz function f and mass m > 0, the bound
p ↦ ‖f p.2.1‖ * ‖f‖_∞ * exp(-p.1 * m²) * H(p.1, ‖Θ p.2.1 - p.2.2‖)
is integrable on (Ioi 0) × SpaceTime × SpaceTime.
Proof structure: Using Tonelli's theorem in the order (y, x, s):
- ∫_y H(s, ‖Θx - y‖) dy = 1 (heat kernel L¹ normalization by translation)
- ∫x ‖f x‖ dx = ‖f‖{L¹} < ∞ (Schwartz integrability)
- ∫s exp(-sm²) ds = 1/m² < ∞ (exponential decay) Total: ‖f‖∞ × ‖f‖_{L¹} / m² < ∞
The proof combines:
heatKernelPositionSpace_integral_translatedfor heat kernel normalizationSchwartzMap.integrablefor Schwartz L¹ integrabilityintegral_exp_neg_mul_Ioi_eq_invfor exponential integral
The proof delegates to schwinger_bound_integrable_fubini for the technical Tonelli step.
Proves that s⁻² * exp(-a/s) is integrable on (0, ∞) by substituting z = 1/s.
The key insight is that with f(s) = s⁻¹:
- f '' (0,∞) = (0,∞)
- f is antitone on (0,∞)
- f'(s) = -s⁻², so -f'(s) = s⁻²
- Under substitution z = 1/s: s⁻² * exp(-a/s) ds becomes exp(-a·z) dz
- ∫₀^∞ exp(-a·z) dz is finite for a > 0
This uses integrableOn_image_iff_integrableOn_deriv_smul_of_antitoneOn.
Dominating function for the Fubini swap in fubini_s_ksp_swap.
Represents the bound C * s^(3/2) * exp(-s(m² + k²)) which comes from:
- Linear vanishing of f at t=0 giving s^(3/2) scaling (offsetting s^(-2) divergence).
- Exponential decay in mass and momentum.
Equations
Instances For
Theoretically proven integrability of dominateG.
Integrable on (0, ∞) × ℝ³ because: ∫ exp(-s|k|²) dk = (π/s)^(3/2). ∫ s^(3/2) * (π/s)^(3/2) * exp(-sm²) ds = π^(3/2) ∫ exp(-sm²) ds. The latter converges for m > 0.
spatialPart is continuous (projection followed by continuous linear equiv).
The integrand for fubini_s_ksp_swap is strongly measurable.
The integrand is:
((s, k_sp), x, y) ↦ fbar(x) · f(y) · √(π/s) · exp(...) · exp(...) · exp(...)
After two applications of StronglyMeasurable.integral_prod_right, the type is:
(((ℝ × SpatialCoords) × SpaceTime) × SpaceTime) → ℂ
represented as x : (ℝ × SpatialCoords) × SpaceTime, y : SpaceTime.
This is a product of continuous/measurable functions, hence measurable.
Heat Kernel Moment Bounds #
The key technical result for hF_le_G is computing the Gaussian moment integral:
∫∫_{x₀,y₀>0} x₀ · y₀ · √(π/s) · exp(-(x₀+y₀)²/(4s)) dx₀ dy₀ = (4/3)√π · s^{3/2}
This is done via change of variables u = x₀ + y₀, v = x₀ - y₀ and standard Gaussian integrals.
The 1D Gaussian integral ∫₀^∞ u³ exp(-u²/(4s)) du = 8s² for s > 0.
This follows from the general formula ∫₀^∞ u^n exp(-au²) du using Gamma functions.
Proof:
Using integral_rpow_mul_exp_neg_mul_rpow with p=2, q=3, b=1/(4s):
- ∫ u³ exp(-b·u²) du = b^(-(3+1)/2) * (1/2) * Γ((3+1)/2)
- = b^(-2) * (1/2) * Γ(2)
- = (4s)² * (1/2) * 1 [since Γ(2) = 1]
- = 8s²
Triangular Fubini identity for the quadrant-to-triangle change of variables
For non-negative integrable f, the change of variables u = x + y transforms the integral over the first quadrant {(x,y) : x > 0, y > 0} to an integral over the triangular region {(x,u) : u > 0, 0 < x < u}:
∫{x>0} ∫{y>0} f(x, x+y) dy dx = ∫{u>0} ∫{0<x<u} f(x, u) dx du
This is a standard result from Fubini-Tonelli theorem. The Jacobian of the map (x, y) ↦ (x, u) where u = x + y has determinant 1.
Proof sketch:
- Both regions have the same measure under the product Lebesgue measure
- The map (x, y) ↦ (x, x+y) is measure-preserving (shear with det = 1)
- Apply Fubini to swap the order of integration
The double Gaussian moment integral: ∫∫_{x₀,y₀>0} x₀·y₀·√(π/s)·exp(-(x₀+y₀)²/(4s)) dx₀ dy₀ = (4/3)√π · s^{3/2}
This is the key bound relating linear vanishing of f at t=0 to the s^{3/2} scaling in dominateG.
Proof (following user's verification): Let J be the integral. Change variables: u = x₀ + y₀. For fixed u, x₀ ranges from 0 to u, and y₀ = u - x₀. Jacobian = 1.
J = √(π/s) ∫₀^∞ exp(-u²/(4s)) [∫₀ᵘ x₀(u - x₀) dx₀] du
Inner integral: ∫₀ᵘ (ux₀ - x₀²) dx₀ = [ux₀²/2 - x₀³/3]₀ᵘ = u³/2 - u³/3 = u³/6
So: J = √(π/s) · (1/6) · ∫₀^∞ u³ exp(-u²/(4s)) du = √(π/s) · (1/6) · 8s² [by integral_u_cubed_gaussian] = √π · s^(-1/2) · (4/3) · s² = (4/3)√π · s^(3/2)
Bound version: The double Gaussian moment integral is bounded by a constant times s^{3/2}.
This is a weaker form of heat_kernel_moment_integral that suffices for
F_norm_bound_via_linear_vanishing.
The exact value is (4/3)√π · s^{3/2}, so we use 10 · s^{3/2} as a comfortable upper bound.
Proof: Uses heat_kernel_moment_integral and the bound (4/3)√π < 10.
Helper lemma: t * exp(-b*t²) is integrable on (0, ∞) for b > 0.
This follows from integrable_mul_exp_neg_mul_sq restricted to positive reals.
Helper lemma: For s > 0 and any t₁ ≥ 0, the function t₂ ↦ t₂ * exp(-(t₁+t₂)²/(4s)) is integrable on (0, ∞). This is the key integrability fact for heat kernel moment bounds.
Proof: For t₁, t₂ ≥ 0, we have (t₁+t₂)² ≥ t₂², so
exp(-(t₁+t₂)²/(4s)) ≤ exp(-t₂²/(4s)), and the integrand is dominated by
t₂ * exp(-t₂²/(4s)) which is integrable by gaussian_moment_integrableOn_Ioi.
The heat kernel moment integrand is integrable on the product quadrant (0,∞)². This is the key integrability result extracted from heat_kernel_moment_integral.
Heat Kernel Moment - Extended by Zero #
The key technique for proving integrability of parametric set integrals is to extend the integrand to be zero outside the region of interest, then use global Fubini theorems.
Heat kernel moment integrand extended by zero outside (0,∞)². F(t₁, t₂) = t₁ · t₂ · √(π/s) · exp(-(t₁+t₂)²/(4s)) for t₁, t₂ > 0, else 0.
Equations
Instances For
The extended heat kernel moment function is integrable on ℝ².
Proof: The function is nonnegative and has finite integral (equal to (π/2)·s^{3/2} by heat_kernel_moment_integral), hence integrable.
Mathematical justification: For nonnegative measurable f, ∫ f < ∞ implies Integrable f (Tonelli's theorem). Here f = heatKernelMomentExt and ∫ f = (π/2)·s^{3/2}.
Reference: Rudin "Real and Complex Analysis" Ch.8 (Tonelli).
Parametric integral of extended heat kernel moment is integrable on ℝ.
This follows from Fubini's theorem: if f is integrable on the product, then t₁ ↦ ∫ t₂, f(t₁, t₂) is integrable.
The parametric integral of the extended function gives a set integral for t₁ > 0.
Key lemma: The parametric set integral of heat kernel moments is integrable on (0,∞).
For any constant c ≥ 0, the function t₁ ↦ ∫_{t₂ > 0} c·t₁·t₂·K(t₁,t₂) dt₂ is integrable on (0,∞).
Proof sketch:
- heatKernelMomentExt is integrable on ℝ² (sorry - uses Tonelli + finite integral)
- By Fubini, t₁ ↦ ∫ t₂, heatKernelMomentExt(t₁,t₂) is integrable on ℝ
- The set integral on (0,∞) equals the full integral (zero outside)
- Multiply by constant c preserves integrability
Fubini factorization for Schwartz functions with linear vanishing.
For Schwartz f : SpaceTime → ℂ vanishing at t ≤ 0, the double integral with heat kernel factor is bounded by K · s^{3/2} for some constant K > 0.
Proof strategy (Tonelli factorization):
- Use
spatialNormIntegral_linear_bound: G(t) := ∫_{ℝ³} ‖f(t,x)‖ dx ≤ C_sp · t - Factor via Tonelli: ∫∫{SpaceTime²} = ∫{time²} G(t₁)·G(t₂) · √(π/s)·exp(...)
- Bound: ≤ C_sp² · ∫_{time²} t₁·t₂ · √(π/s)·exp(-(t₁+t₂)²/(4s))
- Apply
heat_kernel_moment_integral_bound: ≤ C_sp² · 10 · s^{3/2}
Reference: Rudin "Real and Complex Analysis" Ch.8 (Fubini); Standard heat kernel estimates.
Schwartz norm–Gaussian product measurability.
For Schwartz f : SpaceTime → ℂ, constants c₁, c₂ ∈ ℝ, s > 0, and fixed x : SpaceTime, the function a ↦ ‖f x‖ * ‖f a‖ * c₁ * exp(-(x₀ + a₀)²/(4s)) * c₂ is AEStronglyMeasurable.
Mathematical content: This is standard: norms of Schwartz functions are continuous (hence measurable), Gaussian functions are continuous, and products/scalar multiples of measurable functions are measurable.
Reference: Rudin "Real and Complex Analysis" Ch.1 (measurable functions); Folland "Real Analysis" Ch.2.
Iterated integral integrability for Schwartz-bounded functions.
For Schwartz f : SpaceTime → ℂ and bounded factors (√(π/s), exp(-sω²)), the function x ↦ ∫_y ‖f x‖ · ‖f y‖ · √(π/s) · exp(-(x₀+y₀)²/(4s)) · exp(-sω²) is integrable.
Mathematical content: By Fubini/Tonelli, if ∫∫ |F(x,y)| < ∞, then ∫_y |F(x,y)| is integrable in x. Here F(x,y) = ‖f x‖ · ‖f y‖ · (bounded factors), and the double integral is finite by spacetime_fubini_linear_vanishing_bound (using linear vanishing) or by direct Schwartz decay estimates.
Reference: Rudin "Real and Complex Analysis" Ch.8 (Fubini); Folland "Real Analysis" Ch.2 (Tonelli).
Bound on F(s, k_sp) using linear vanishing of f.
For f vanishing at t ≤ 0 with |f(x)| ≤ C·x₀, we have: |F(s, k_sp)| ≤ C² · (4/3)√π · s^{3/2} · exp(-s(‖k_sp‖² + m²))
The constant 100 in dominateG provides ample room for the (4/3)√π ≈ 2.36 factor.
Proof sketch:
- From
schwartz_vanishing_linear_bound: |f(x)| ≤ C·x₀ for x₀ > 0 - Triangle inequality: |F| ≤ ∫∫ |f(x)||f(y)| · √(π/s) · |exp(...)| dx dy
- Key: |exp(-i·...)| = 1, and |f(x)||f(y)| ≤ C²·x₀·y₀
- Heat kernel moment integral: ∫∫ x₀·y₀·√(π/s)·exp(-(x₀+y₀)²/(4s)) = (4/3)√π·s^{3/2}
- Combine: ≤ C² · (4/3)√π · s^{3/2} · exp(-s(‖k‖²+m²)) < 100 · f_L1² · s^{3/2} · exp(...)
The detailed calculation is mathematically standard but technically involved.
See heat_kernel_moment_integral for the key integral evaluation.
Mathematical justification: The bound uses the linear vanishing property |f(x)| ≤ C·x₀ for x₀ > 0, which combined with heat_kernel_moment_integral gives |F| ≤ C² · (4/3)√π · s^{3/2} · exp(-sω²). The constant C comes from schwartz_vanishing_linear_bound (derivative bound via MVT).
Fubini swap for s ↔ pbar integrals.
Swaps integration order: ∫₀^∞ ds ∫_ℝ³ d³pbar F(s, pbar) = ∫_ℝ³ d³pbar ∫₀^∞ ds F(s, pbar)
where the integrand contains:
- √(π/s) · exp(-t²/(4s)) from the k₀ Gaussian integral
- exp(-s(|pbar|² + m²)) from the spatial momentum and mass
- exp(-ipbar·rbar) phase factor
Justification: Fubini applies because:
- The pbar-dependence is Schwartz (Fourier transform of Schwartz test functions)
- The s-integrand decays as exp(-s·ω²) where ω² = |pbar|² + m² > 0
- Combined integrability on ℝ³ × (0,∞) follows from
Integrable.prod_mul
Note: This is the most delicate step. Requires splitting the region into "small s" (UV, controlling 1/r² singularity) and "large s" (IR, using mass m).
Validation: Reviewed by Gemini 3 Pro - confirmed mathematically valid, assuming m > 0 which ensures exponential decay at large s for all k_sp.
Key integrability lemma: Uses integrable_s_inv_sq_exp_neg_inv_s to
handle the s^{-1/2} * exp(-t²/(4s)) term via substitution z = 1/s.
Schwartz function norm is integrable.
Product of Schwartz norms is integrable on SpaceTime × SpaceTime.
Fubini swap for s ↔ (x,y) integrals (for fixed k_sp).
For fixed k_sp, swaps integration order: ∫₀^∞ ds ∫_x ∫_y F(s,x,y) = ∫_x ∫_y ∫₀^∞ ds F(s,x,y)
Proof: Uses MeasureTheory.integral_integral_swap with
integrability on (Set.Ioi 0) × SpaceTime × SpaceTime.
The bound function is s^{-1/2} * exp(-s*m^2) * |f(x)| * |f(y)|.
Fubini Helper Lemmas #
These lemmas establish the integrability needed for Fubini swaps in the reflection positivity proof. The key observation is that:
- Schwartz functions are L¹: ∫|f(x)| dx < ∞
- Gaussians are L¹: ∫ exp(-s‖k‖²) dk = (π/s)^{n/2}
- Products of L¹ functions on independent spaces are L¹ on the product
The common bound for all Fubini swaps is: |integrand| ≤ |f(x)| |f(y)| × C(s) × exp(-s‖k_sp‖²) which factors and is therefore integrable on the product space.
The Gaussian exp(-s‖k‖²) is integrable over SpatialCoords for s > 0.
Key Lemma: The integrand for fubini_ksp_xy_swap is absolutely integrable.
The bound |f(x)| |f(y)| exp(-s‖k_sp‖²) is integrable on SpatialCoords × SpaceTime × SpaceTime because:
- ∫_{k_sp} exp(-s‖k_sp‖²) dk_sp = (π/s)^{3/2} < ∞
- ∫∫_{x,y} |f(x)| |f(y)| dx dy = ‖f‖₁² < ∞
- The product factorizes on independent spaces
The full Fubini integrand is absolutely integrable on SpatialCoords × SpaceTime × SpaceTime.
The integrand is: fbar(x) · f(y) · √(π/s) · exp(-t²/4s) · exp(-s‖k_sp‖²) · exp(-ik·r)
Bound: |integrand| ≤ |f(x)| · |f(y)| · √(π/s) · 1 · exp(-s‖k_sp‖²) · 1 = √(π/s) · |f(x)| · |f(y)| · exp(-s‖k_sp‖²)
This is a constant multiple of fubini_ksp_xy_integrand_integrable.
Proof sketch: Apply Integrable.mono' with the bound function
√(π/s) * ‖f(x)‖ * ‖f(y)‖ * exp(-s‖k_sp‖²), which is integrable by
fubini_ksp_xy_integrand_integrable. The norm bounds follow from:
- |starRingEnd ℂ (f x)| = |f x|
- |ofReal (√(π/s))| = √(π/s) (non-negative)
- |exp(negative real)| ≤ 1
- |exp(pure imaginary)| = 1
Fubini swap for k_sp ↔ (x,y) integrals.
For fixed s > 0, swaps integration order: ∫x ∫y (... * ∫{k_sp} F) = ∫{k_sp} ∫_x ∫_y (... * F)
This moves the spatial momentum integral k_sp from inside the spacetime integrals (x,y) to outside them.
Proof: Two steps:
- Pull the k_sp integral out: A(x,y) * ∫{k_sp} B = ∫{k_sp} A(x,y) * B
- Apply Fubini (integral_integral_swap) to swap x,y,k_sp to k_sp,x,y