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} : (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.

def SpaceTime.timeSliceLinearEquiv {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] : (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 = { toFun := ⇑SpaceTime.timeSlice, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑SpaceTime.timeSlice.symm, left_inv := ⋯, right_inv := ⋯ }

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

theorem SpaceTime.timeSliceLinearEquiv_symm_apply {d : ℕ} {M : Type} [AddCommGroup M] [Module ℝ M] (f : Time → Space d → M) : timeSliceLinearEquiv.symm f = timeSlice.symm f

theorem SpaceTime.timeSlice_spatial_deriv {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} {f : SpaceTime d → M} {t : Time} {x : Space d} (hdiff : DifferentiableAt ℝ f (toTimeAndSpace.symm (t, x))) (i : Fin d) : timeSlice (deriv (Fin.natAdd 1 i) f) t x = Space.deriv i (timeSlice f t) x

The derivative on space commutes with time-slicing.

theorem SpaceTime.timeSlice_time_deriv {M : Type} [NormedAddCommGroup M] [NormedSpace ℝ M] {d : ℕ} (f : SpaceTime d → M) {t : Time} {x : Space d} (hdiff : DifferentiableAt ℝ f (toTimeAndSpace.symm (t, x))) : timeSlice (deriv (finSumFinEquiv (Sum.inl 0)) f) t x = Time.deriv (fun (t : Time) => timeSlice f t x) t

The derivative on time commutes with time-slicing.