SpaceTime-specialized version

For SpaceTime = EuclideanSpace ℝ (Fin 4), the time coordinate is accessed via x 0. This specialized version matches the signature needed in OS3_MixedRepInfra.lean.

theorem schwartz_vanishing_linear_bound (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : ∃ (C : ℝ), 0 < C ∧ ∀ (x : SpaceTime), 0 < x.ofLp 0 → ‖f x‖ ≤ C * x.ofLp 0

For a Schwartz function vanishing on {x₀ ≤ 0}, the linear bound ‖f(x)‖ ≤ C · x₀ holds. Follows from mean value theorem + global derivative bounds on Schwartz functions.

Integrate over space first (Fubini approach)

The key insight is to decompose SpaceTime = ℝ × ℝ³ and integrate over spatial coordinates first. For a Schwartz function f : SpaceTime → ℂ vanishing at t ≤ 0:

1. Define G(t) = ∫_{ℝ³} ‖f(t, x)‖ dx (the spatial integral of the norm)
2. G is well-defined and finite for all t (f is Schwartz)
3. G(t) = 0 for t ≤ 0 (f vanishes there)
4. G satisfies a linear bound: G(t) ≤ C·t for t > 0

Then by Fubini/Tonelli: ∫∫ ‖f(p₁)‖·‖f(p₂)‖/(t₁+t₂)² = ∫∫ G(t₁)·G(t₂)/(t₁+t₂)² dt₁ dt₂

Using G(t) ≤ C·t and AM-GM: t₁t₂/(t₁+t₂)² ≤ 1/4, the integrand is ≤ C²/4. On the bounded time domain {0 < t₁, 0 < t₂, t₁+t₂ < 1}, this gives integrability.

@[reducible, inline]

abbrev SpatialCoords3 : Type

The spatial part of SpaceTime: ℝ³.

Equations

• SpatialCoords3 = EuclideanSpace ℝ (Fin 3)

noncomputable def spacetimeOfTimeSpace (t : ℝ) (x : SpatialCoords3) : SpaceTime

Decomposition of SpaceTime as time × space.

Equations

• spacetimeOfTimeSpace t x = (EuclideanSpace.equiv (Fin 4) ℝ).symm (Fin.cons t fun (i : Fin 3) => x.ofLp i)

theorem spacetimeOfTimeSpace_time (t : ℝ) (x : SpatialCoords3) : (spacetimeOfTimeSpace t x).ofLp 0 = t

The time coordinate of spacetimeOfTimeSpace is t.

theorem spacetimeOfTimeSpace_spatial (t : ℝ) (x : SpatialCoords3) (i : Fin 3) : (spacetimeOfTimeSpace t x).ofLp ⟨↑i + 1, ⋯⟩ = x.ofLp i

Access the i-th spatial component of spacetimeOfTimeSpace. Mathematical fact: (spacetimeOfTimeSpace t x) (i+1) = x i

theorem spacetimeOfTimeSpace_decompose (t : ℝ) (x : SpatialCoords3) : spacetimeOfTimeSpace t x = spacetimeOfTimeSpace t 0 + spacetimeOfTimeSpace 0 x

The decomposition: spacetimeOfTimeSpace t x = timeOrigin t + spatialEmbed x. This is the key structural fact: (t, x) = (t, 0) + (0, x).

theorem spacetimeOfTimeSpace_norm_ge (t : ℝ) (x : SpatialCoords3) : ‖spacetimeOfTimeSpace t x‖ ≥ ‖x‖

Norm comparison: the spacetime norm dominates the spatial norm.

noncomputable def spatialEmbed : SpatialCoords3 →ₗ[ℝ] SpaceTime

Linear embedding of ℝ³ into ℝ⁴ as the spatial subspace at time 0. This maps x ↦ (0, x₀, x₁, x₂), i.e., spacetimeOfTimeSpace 0 x.

Equations

• spatialEmbed = { toFun := fun (x : SpatialCoords3) => spacetimeOfTimeSpace 0 x, map_add' := spatialEmbed._proof_1, map_smul' := spatialEmbed._proof_2 }

theorem spatialEmbed_continuous : Continuous ⇑spatialEmbed

The spatial embedding is continuous (being linear on finite-dim spaces).

noncomputable def spatialEmbedCLM : SpatialCoords3 →L[ℝ] SpaceTime

The spatial embedding as a CLM.

Equations

• spatialEmbedCLM = { toLinearMap := spatialEmbed, cont := spatialEmbed_continuous }

noncomputable def timeOrigin (t : ℝ) : SpaceTime

The time-origin point: (t, 0, 0, 0) in SpaceTime.

Equations

• timeOrigin t = spacetimeOfTimeSpace t 0

theorem continuous_spacetimeOfTimeSpace_right (t : ℝ) : Continuous (spacetimeOfTimeSpace t)

spacetimeOfTimeSpace is continuous in the spatial argument for fixed time.

theorem schwartz_time_slice_integrable (f : TestFunctionℂ) (t : ℝ) : MeasureTheory.Integrable (fun (x : SpatialCoords3) => f (spacetimeOfTimeSpace t x)) MeasureTheory.volume

A Schwartz function restricted to a fixed time slice is integrable over ℝ³. Uses decay transfer: 4D Schwartz decay implies 3D integrability via norm comparison.

noncomputable def spatialNormIntegral (f : TestFunctionℂ) (t : ℝ) : ℝ

The spatial integral G(t) = ∫_{ℝ³} ‖f(t, x)‖ dx.

Equations

• spatialNormIntegral f t = ∫ (x : SpatialCoords3), ‖f (spacetimeOfTimeSpace t x)‖

theorem spatialNormIntegral_zero_of_neg (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) (t : ℝ) (ht : t ≤ 0) : spatialNormIntegral f t = 0

G(t) = 0 for t ≤ 0 when f vanishes on {t ≤ 0}.

theorem spatialNormIntegral_nonneg (f : TestFunctionℂ) (t : ℝ) : 0 ≤ spatialNormIntegral f t

G(t) is nonnegative.

FTC-based decay bound for Schwartz functions vanishing at t=0

theorem schwartz_vanishing_ftc_decay (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 < t → ∀ (x_sp : SpatialCoords3), ‖f (spacetimeOfTimeSpace t x_sp)‖ ≤ C * t / (1 + ‖x_sp‖) ^ 4

Combined FTC + Schwartz decay bound: For a Schwartz function f vanishing at t ≤ 0, we have ‖f(t, x_sp)‖ ≤ C · t / (1 + ‖x_sp‖)^4.

Mathematical content:

Since f(0, x_sp) = 0 for all x_sp (by vanishing condition), the fundamental theorem of calculus gives: f(t, x_sp) = ∫₀^t ∂f/∂τ(τ, x_sp) dτ

Therefore: ‖f(t, x_sp)‖ ≤ ∫₀^t ‖∂f/∂τ(τ, x_sp)‖ dτ ≤ t · sup_{τ∈[0,t]} ‖∂f/∂τ(τ, x_sp)‖

The time derivative ∂f/∂τ is also Schwartz (derivatives of Schwartz functions are Schwartz), so it has fast spatial decay. For τ in any bounded interval [0, T]: ‖∂f/∂τ(τ, x_sp)‖ ≤ C_deriv / (1 + ‖x_sp‖)^4

Combining: ‖f(t, x_sp)‖ ≤ t · C_deriv / (1 + ‖x_sp‖)^4

Key insight: This bound is BOTH linear in t (from FTC) AND has spatial decay (from Schwartz property of the derivative). This combination is what makes the spatial integral ∫ ‖f(t, ·)‖ dx bounded by C·t.

Used by: spatialNormIntegral_linear_bound and F_norm_bound_via_linear_vanishing.

theorem spatialNormIntegral_linear_bound (f : TestFunctionℂ) (hf_supp : ∀ (x : SpaceTime), x.ofLp 0 ≤ 0 → f x = 0) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 < t → spatialNormIntegral f t ≤ C * t

The key linear bound: G(t) ≤ C·t for t > 0.

This follows from integrating the pointwise bound ‖f(t,x)‖ ≤ C·t over the spatial coordinates. Since Schwartz functions have fast decay, the spatial integral is finite.