1. Physlib
  2. SpaceAndTime
  3. SpaceTime
  4. TimeSlice
Imports
/- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ module public import Physlib.SpaceAndTime.SpaceTime.Derivatives public import Physlib.SpaceAndTime.TimeAndSpace.Basic

Time slice

Time slicing functions on spacetime, turning them into a function Time → Space d → M.

This is useful when going from relativistic physics (defined using SpaceTime) to non-relativistic physics (defined using Space and Time).

@[expose] public section

The timeslice of a function SpaceTime d → M forming a function Time → Space d → M.

def timeSlice {d : ℕ} {M : Type} (c : SpeedOfLight := 1) : (SpaceTime d → M) ≃ (Time → Space d → M) where toFun f := Function.curry (f ∘ (toTimeAndSpace c).symm) invFun f := Function.uncurry f ∘ toTimeAndSpace c left_inv f := d:ℕM:Typec:SpeedOfLightf:SpaceTime d → M⊢ (fun f => Function.uncurry f ∘ ⇑(toTimeAndSpace c)) ((fun f => Function.curry (f ∘ ⇑(toTimeAndSpace c).symm)) f) = f d:ℕM:Typec:SpeedOfLightf:SpaceTime d → Mx:SpaceTime d⊢ (fun f => Function.uncurry f ∘ ⇑(toTimeAndSpace c)) ((fun f => Function.curry (f ∘ ⇑(toTimeAndSpace c).symm)) f) x = f x All goals completed! 🐙 right_inv f := d:ℕM:Typec:SpeedOfLightf:Time → Space d → M⊢ (fun f => Function.curry (f ∘ ⇑(toTimeAndSpace c).symm)) ((fun f => Function.uncurry f ∘ ⇑(toTimeAndSpace c)) f) = f d:ℕM:Typec:SpeedOfLightf:Time → Space d → Mx:Timet:Space d⊢ (fun f => Function.curry (f ∘ ⇑(toTimeAndSpace c).symm)) ((fun f => Function.uncurry f ∘ ⇑(toTimeAndSpace c)) f) x t = f x t All goals completed! 🐙
@[fun_prop] lemma timeSlice_contDiff {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {n} (c : SpeedOfLight) (f : SpaceTime d → M) (h : ContDiff ℝ n f) : ContDiff ℝ n ↿(timeSlice c f) := d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n ↿((timeSlice c) f) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n (f ∘ ⇑(toTimeAndSpace c).symm) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n fd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n ⇑(toTimeAndSpace c).symm d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n f All goals completed! 🐙 d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:SpaceTime d → Mh:ContDiff ℝ n f⊢ ContDiff ℝ n ⇑(toTimeAndSpace c).symm All goals completed! 🐙@[fun_prop] lemma timeSlice_differentiable {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) (h : Differentiable ℝ f) : Differentiable ℝ ↿(timeSlice c f) := d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ ↿((timeSlice c) f) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ (f ∘ ⇑(toTimeAndSpace c).symm) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ fd:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ ⇑(toTimeAndSpace c).symm d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ f All goals completed! 🐙 d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:SpaceTime d → Mh:Differentiable ℝ f⊢ Differentiable ℝ ⇑(toTimeAndSpace c).symm All goals completed! 🐙@[fun_prop] lemma timeSlice_symm_contDiff {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {n} (c : SpeedOfLight) (f : Time → Space d → M) (h : ContDiff ℝ n ↿f) : ContDiff ℝ n ((timeSlice c).symm f) := d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n ((timeSlice c).symm f) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n (Function.uncurry f ∘ ⇑(toTimeAndSpace c)) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n (Function.uncurry f)d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n ⇑(toTimeAndSpace c) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n (Function.uncurry f) All goals completed! 🐙 d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mn:WithTop ℕ∞c:SpeedOfLightf:Time → Space d → Mh:ContDiff ℝ n ↿f⊢ ContDiff ℝ n ⇑(toTimeAndSpace c) All goals completed! 🐙@[fun_prop] lemma timeSlice_symm_differentiable {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : Time → Space d → M) (h : Differentiable ℝ ↿f) : Differentiable ℝ ↿((timeSlice c).symm f) := d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ ↿((timeSlice c).symm f) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ (Function.uncurry f ∘ ⇑(toTimeAndSpace c)) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ (Function.uncurry f)d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ ⇑(toTimeAndSpace c) d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ (Function.uncurry f) All goals completed! 🐙 d:ℕM:Typeinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:Time → Space d → Mh:Differentiable ℝ ↿f⊢ Differentiable ℝ ⇑(toTimeAndSpace c) All goals completed! 🐙

The timeslice of a function SpaceTime d → M forming a function Time → Space d → M, as a linear equivalence.

def timeSliceLinearEquiv {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (c : SpeedOfLight := 1) : (SpaceTime d → M) ≃ₗ[ℝ] (Time → Space d → M) where toFun := timeSlice c invFun := (timeSlice c).symm map_add' f g := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:SpaceTime d → Mg:SpaceTime d → M⊢ (timeSlice c) (f + g) = (timeSlice c) f + (timeSlice c) g d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:SpaceTime d → Mg:SpaceTime d → Mt:Timex:Space d⊢ (timeSlice c) (f + g) t x = ((timeSlice c) f + (timeSlice c) g) t x All goals completed! 🐙 map_smul' := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLight⊢ ∀ (m : ℝ) (x : SpaceTime d → M), (timeSlice c) (m • x) = (RingHom.id ℝ) m • (timeSlice c) x d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc✝:SpeedOfLightc:ℝf:SpaceTime d → M⊢ (timeSlice c✝) (c • f) = (RingHom.id ℝ) c • (timeSlice c✝) f d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc✝:SpeedOfLightc:ℝf:SpaceTime d → Mt:Timex:Space d⊢ (timeSlice c✝) (c • f) t x = ((RingHom.id ℝ) c • (timeSlice c✝) f) t x All goals completed! 🐙 left_inv f := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:SpaceTime d → M⊢ (timeSlice c).symm ((timeSlice c) f) = f All goals completed! 🐙 right_inv f := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:Time → Space d → M⊢ (timeSlice c) ((timeSlice c).symm f) = f All goals completed! 🐙
lemma timeSliceLinearEquiv_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) : timeSliceLinearEquiv c f = timeSlice c f := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:SpaceTime d → M⊢ (timeSliceLinearEquiv c) f = (timeSlice c) f All goals completed! 🐙lemma timeSliceLinearEquiv_symm_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (c : SpeedOfLight) (f : Time → Space d → M) : (timeSliceLinearEquiv c).symm f = (timeSlice c).symm f := d:ℕM:Typeinst✝¹:AddCommGroup Minst✝:Module ℝ Mc:SpeedOfLightf:Time → Space d → M⊢ (timeSliceLinearEquiv c).symm f = (timeSlice c).symm f All goals completed! 🐙

B. Time slices of distributions

lemma distTimeSlice_apply {M d} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : (SpaceTime d) →d[ℝ] M) (κ : 𝓢(Time × Space d, ℝ)) : distTimeSlice c f κ = f (compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c) κ) := M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)⊢ ((distTimeSlice c) f) κ = f ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) κ) All goals completed! 🐙lemma distTimeSlice_symm_apply {M d} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : (Time × (Space d)) →d[ℝ] M) (κ : 𝓢(SpaceTime d, ℝ)) : (distTimeSlice c).symm f κ = f (compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c).symm κ) := M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(Time × Space d)→d[ℝ] Mκ:𝓢(SpaceTime d, ℝ)⊢ ((distTimeSlice c).symm f) κ = f ((compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c).symm) κ) All goals completed! 🐙

B.1. Time slices and derivatives

M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ (1 / c.val) • (fderiv ℝ (⇑κ) ((toTimeAndSpace c) x)) (1, 0) = c.val⁻¹ * (fderiv ℝ (⇑κ) ((toTimeAndSpace c) x)) (1, 0)M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑κ) ((toTimeAndSpace c) x)M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(toTimeAndSpace c)) x M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑κ) ((toTimeAndSpace c) x)M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(toTimeAndSpace c)) x M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑κ) ((toTimeAndSpace c) x) M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ Differentiable ℝ ⇑κ All goals completed! 🐙 M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(toTimeAndSpace c)) x All goals completed! 🐙M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(SpaceTime d)→d[ℝ] M⊢ (1 / c.val) • distTimeDeriv ((distTimeSlice c) f) = c.val⁻¹ • distTimeDeriv ((distTimeSlice c) f) All goals completed! 🐙M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLightf:(Time × Space d)→d[ℝ] M⊢ (distTimeSlice c).symm (distTimeDeriv f) = c.val • (1 / c.val) • (distTimeSlice c).symm (distTimeDeriv f) All goals completed! 🐙M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLighti:Fin df:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑κ) ((toTimeAndSpace c) x)M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLighti:Fin df:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(toTimeAndSpace c)) x M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLighti:Fin df:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑κ) ((toTimeAndSpace c) x) M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLighti:Fin df:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ Differentiable ℝ ⇑κ All goals completed! 🐙 M:Typed:ℕinst✝¹:NormedAddCommGroup Minst✝:NormedSpace ℝ Mc:SpeedOfLighti:Fin df:(SpaceTime d)→d[ℝ] Mκ:𝓢(Time × Space d, ℝ)x:SpaceTime d⊢ DifferentiableAt ℝ (⇑(toTimeAndSpace c)) x All goals completed! 🐙All goals completed! 🐙