Spacetime Decomposition

This file provides the measure-preserving decomposition of SpaceTime into time and spatial components: SpaceTime ≃ᵐ ℝ × SpatialCoords.

Main Definitions

• piLpMeasurableEquiv - MeasurableEquiv between PiLp and underlying pi type
• spacetimeDecomp - The measurable equivalence SpaceTime ≃ᵐ ℝ × SpatialCoords

Main Results

• spacetimeDecomp_measurePreserving - The decomposition preserves Lebesgue measure
• spacetimeDecomp_apply - Explicit formula: spacetimeDecomp k = (k 0, spatialPart k)
• spacetime_norm_sq_decompose - Norm decomposition: ‖k‖² = k₀² + ‖k_sp‖²

Integral Decomposition for SpaceTime

We establish that integrals over SpaceTime can be decomposed into iterated integrals over ℝ (time component) and SpatialCoords (spatial components). This uses MeasurableEquiv.piFinSuccAbove and measurePreserving_piFinSuccAbove.

def piLpMeasurableEquiv (n : ℕ) : (PiLp 2 fun (x : Fin n) => ℝ) ≃ᵐ (Fin n → ℝ)

MeasurableEquiv between PiLp and the underlying pi type.

Equations

• piLpMeasurableEquiv n = { toEquiv := WithLp.equiv 2 ((i : Fin n) → (fun (x : Fin n) => ℝ) i), measurable_toFun := ⋯, measurable_invFun := ⋯ }

def spacetimeDecomp : SpaceTime ≃ᵐ ℝ × SpatialCoords

The measurable equivalence from SpaceTime to ℝ × SpatialCoords. Composes three measure-preserving maps:

1. piLpMeasurableEquiv : EuclideanSpace ℝ (Fin 4) → (Fin 4 → ℝ)
2. piFinSuccAbove 0 : (Fin 4 → ℝ) → ℝ × (Fin 3 → ℝ)
3. id × piLpMeasurableEquiv.symm : ℝ × (Fin 3 → ℝ) → ℝ × SpatialCoords

Equations

• One or more equations did not get rendered due to their size.

theorem piLpMeasurableEquiv_measurePreserving (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(piLpMeasurableEquiv n)) MeasureTheory.volume MeasureTheory.volume

Measure preservation for piLpMeasurableEquiv.

theorem spacetimeDecomp_measurePreserving : MeasureTheory.MeasurePreserving (⇑spacetimeDecomp) MeasureTheory.volume MeasureTheory.volume

The spacetime decomposition preserves measure.

theorem spacetimeDecomp_apply (k : SpaceTime) : spacetimeDecomp k = (k.ofLp 0, spatialPart k)

Spacetime decomposition maps k to (k 0, spatialPart k).

theorem spacetimeDecomp_symm_eq_spacetimeOfTimeSpace (t : ℝ) (v : SpatialCoords) : spacetimeDecomp.symm (t, v) = spacetimeOfTimeSpace t v

spacetimeDecomp.symm equals spacetimeOfTimeSpace (from SchwartzProdIntegrable.lean). Both construct a SpaceTime point from time t and spatial coordinates v.

theorem spacetime_norm_sq_decompose (k : SpaceTime) : ‖k‖ ^ 2 = k.ofLp 0 ^ 2 + ‖spatialPart k‖ ^ 2

The SpaceTime norm decomposes into time and spatial parts: ‖k‖² = k₀² + ‖k_sp‖².

theorem integral_spacetime_prod_split {f : ℝ → ℂ} {g : SpatialCoords → ℂ} (_hf : MeasureTheory.Integrable f MeasureTheory.volume) (_hg : MeasureTheory.Integrable g MeasureTheory.volume) : ∫ (k : SpaceTime), f (k.ofLp 0) * g (spatialPart k) = (∫ (k₀ : ℝ), f k₀) * ∫ (k_sp : SpatialCoords), g k_sp

For a product-type integrand f(k₀) × g(k_sp), the integral decomposes as a product.