Schwartz Tonelli Factorization

This file proves the Tonelli factorization theorem for Schwartz functions on SpaceTime, which states that double integrals over SpaceTime can be factorized when the kernel depends only on the time coordinates.

Main Results

• schwartz_tonelli_spacetime - Tonelli factorization for Schwartz functions on SpaceTime

References

• Hörmander, "The Analysis of Linear Partial Differential Operators I"
• Folland, "Real Analysis", Chapter 2 (Fubini-Tonelli theorem)

Auxiliary Lemmas

theorem spacetimeDecomp_symm_norm_ge (t : ℝ) (v : SpatialCoords) : ‖spacetimeDecomp.symm (t, v)‖ ≥ ‖v‖

Norm bound: ‖spacetimeDecomp.symm (t, v)‖ ≥ ‖v‖. This follows from: ‖x‖² = t² + ‖v‖² ≥ ‖v‖².

theorem schwartz_slice_integrable (f : SchwartzMap SpaceTime ℂ) (t : ℝ) : MeasureTheory.Integrable (fun (v : SpatialCoords) => ‖f (spacetimeDecomp.symm (t, v))‖) MeasureTheory.volume

Slice integrability: for fixed t, the slice is integrable over SpatialCoords.

theorem schwartz_integrable_on_prod' (f : SchwartzMap SpaceTime ℂ) : MeasureTheory.Integrable (fun (p : ℝ × SpatialCoords) => ‖f (spacetimeDecomp.symm p)‖) MeasureTheory.volume

Schwartz composed with spacetimeDecomp.symm is integrable on the product.

Main Theorem

theorem schwartz_tonelli_spacetime (f g : SchwartzMap SpaceTime ℂ) (K : ℝ → ℝ → ℝ) (hK_nn : ∀ (t₁ t₂ : ℝ), 0 ≤ K t₁ t₂) (hK_meas : Measurable (Function.uncurry K)) (hK_bdd : ∃ (C : ℝ), ∀ (t₁ t₂ : ℝ), K t₁ t₂ ≤ C) : have G_f := fun (t : ℝ) => ∫ (v : SpatialCoords), ‖f (spacetimeDecomp.symm (t, v))‖; have G_g := fun (t : ℝ) => ∫ (v : SpatialCoords), ‖g (spacetimeDecomp.symm (t, v))‖; ∫ (x : SpaceTime) (y : SpaceTime), ‖f x‖ * ‖g y‖ * K (x.ofLp 0) (y.ofLp 0) = ∫ (t₁ : ℝ) (t₂ : ℝ), K t₁ t₂ * G_f t₁ * G_g t₂

Tonelli factorization for SpaceTime.

For Schwartz functions f, g on SpaceTime and a bounded non-negative measurable kernel K depending only on time coordinates, the double integral factors:

∫∫ ‖f x‖ · ‖g y‖ · K(x₀, y₀) dx dy = ∫∫ K(t₁, t₂) · G_f(t₁) · G_g(t₂) dt₁ dt₂

where G_f(t) = ∫ ‖f(t, v)‖ dv is the spatial integral at time t.

This is a key tool for establishing reflection positivity (OS3) bounds.