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).

def SpaceTime.timeSlice {d : ℕ} {M : Type} (c : SpeedOfLight := 1) : (SpaceTime d → M) ≃ (Time → Space d → M)

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

Equations

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

theorem SpaceTime.timeSlice_contDiff {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {n : WithTop ℕ∞} (c : SpeedOfLight) (f : SpaceTime d → M) (h : ContDiff ℝ n f) : ContDiff ℝ n ↿((timeSlice c) f)

theorem SpaceTime.timeSlice_differentiable {d : ℕ} {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) (h : Differentiable ℝ f) : Differentiable ℝ ↿((timeSlice c) f)

def SpaceTime.timeSliceLinearEquiv {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (c : SpeedOfLight := 1) : (SpaceTime d → M) ≃ₗ[ℝ] Time → Space d → M

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

Equations

• SpaceTime.timeSliceLinearEquiv c = { toFun := ⇑(SpaceTime.timeSlice c), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(SpaceTime.timeSlice c).symm, left_inv := ⋯, right_inv := ⋯ }

theorem SpaceTime.timeSliceLinearEquiv_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (c : SpeedOfLight) (f : SpaceTime d → M) : (timeSliceLinearEquiv c) f = (timeSlice c) f

theorem SpaceTime.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

B. Time slices of distributions

noncomputable def SpaceTime.distTimeSlice {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight := 1) : ((SpaceTime d)→d[ℝ] M) ≃L[ℝ] (Time × Space d)→d[ℝ] M

The time slice of a distribution on SpaceTime d to form a distribution on Time × Space d.

Equations

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

theorem SpaceTime.distTimeSlice_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : (SpaceTime d)→d[ℝ] M) (κ : SchwartzMap (Time × Space d) ℝ) : ((distTimeSlice c) f) κ = f ((SchwartzMap.compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c)) κ)

theorem SpaceTime.distTimeSlice_symm_apply {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] (c : SpeedOfLight) (f : (Time × Space d)→d[ℝ] M) (κ : SchwartzMap (SpaceTime d) ℝ) : ((distTimeSlice c).symm f) κ = f ((SchwartzMap.compCLMOfContinuousLinearEquiv ℝ (toTimeAndSpace c).symm) κ)

B.1. Time slices and derivatives

theorem SpaceTime.distTimeSlice_distDeriv_inl {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {c : SpeedOfLight} (f : (SpaceTime d)→d[ℝ] M) : (distTimeSlice c) ((distDeriv (Sum.inl 0)) f) = (1 / c.val) • Space.distTimeDeriv ((distTimeSlice c) f)

theorem SpaceTime.distDeriv_inl_distTimeSlice_symm {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {c : SpeedOfLight} (f : (Time × Space d)→d[ℝ] M) : (distDeriv (Sum.inl 0)) ((distTimeSlice c).symm f) = (1 / c.val) • (distTimeSlice c).symm (Space.distTimeDeriv f)

theorem SpaceTime.distTimeSlice_symm_distTimeDeriv_eq {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {c : SpeedOfLight} (f : (Time × Space d)→d[ℝ] M) : (distTimeSlice c).symm (Space.distTimeDeriv f) = c.val • (distDeriv (Sum.inl 0)) ((distTimeSlice c).symm f)

theorem SpaceTime.distTimeSlice_distDeriv_inr {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {c : SpeedOfLight} (i : Fin d) (f : (SpaceTime d)→d[ℝ] M) : (distTimeSlice c) ((distDeriv (Sum.inr i)) f) = (Space.distSpaceDeriv i) ((distTimeSlice c) f)

theorem SpaceTime.distDeriv_inr_distTimeSlice_symm {M : Type} {d : ℕ} [NormedAddCommGroup M] [NormedSpace ℝ M] {c : SpeedOfLight} (i : Fin d) (f : (Time × Space d)→d[ℝ] M) : (distDeriv (Sum.inr i)) ((distTimeSlice c).symm f) = (distTimeSlice c).symm ((Space.distSpaceDeriv i) f)