PhyslibSearch

Physlib.SpaceAndTime.SpaceTime.TimeSlice

11 declarations

theorem

Time slicing preserves CnC^n differentiability of spacetime functions

#timeSlice_contDiff

Let dd be a natural number representing the spatial dimension, and let MM be a normed real vector space. Given a speed of light cc and a function f:SpaceTime dMf: \text{SpaceTime } d \to M, if ff is nn-times continuously differentiable (CnC^n), then its uncurried time-slice representation—the function mapping the pair of time and space (t,x)Time×Space d(t, x) \in \text{Time} \times \text{Space } d to MM—is also nn-times continuously differentiable.

theorem

Differentiability of the time-sliced function ff

#timeSlice_differentiable

Let dd be a natural number representing the spatial dimension and MM be a real normed space. Given a speed of light cc, let f:SpaceTime dMf: \text{SpaceTime } d \to M be a function. If ff is differentiable over R\mathbb{R}, then its uncurried time-sliced representation F:Time×Space dMF: \text{Time} \times \text{Space } d \to M is also differentiable over R\mathbb{R}.

theorem

timeSliceLinearEquivcf=timeSlicecf\text{timeSliceLinearEquiv}_c f = \text{timeSlice}_c f

#timeSliceLinearEquiv_apply

Let dd be a natural number representing the spatial dimension, and let MM be a real vector space. For a given speed of light cc, the operator timeSliceLinearEquivc\text{timeSliceLinearEquiv}_c is a linear equivalence that transforms a function on spacetime f:SpaceTime dMf : \text{SpaceTime } d \to M into its representation as a function of time and space. This theorem states that the application of this linear equivalence to ff is equal to the direct time-slicing of ff: timeSliceLinearEquivc(f)=timeSlicec(f)\text{timeSliceLinearEquiv}_c(f) = \text{timeSlice}_c(f) where timeSlicec(f)\text{timeSlice}_c(f) is the function of type TimeSpace dM\text{Time} \to \text{Space } d \to M obtained by decomposing the spacetime coordinates.

theorem

The inverse of the linear time-slice equivalence equals the inverse of the time-slice map

#timeSliceLinearEquiv_symm_apply

Let dd be the spatial dimension and MM be a real vector space. For a given speed of light cc, let timeSlicec\text{timeSlice}_c be the operation that transforms a function defined on spacetime into a function from Time\text{Time} to Space d\text{Space } d. Let timeSliceLinearEquivc\text{timeSliceLinearEquiv}_c be the linear equivalence representing this same transformation. For any function f:TimeSpace dMf: \text{Time} \to \text{Space } d \to M, the application of the inverse of the linear equivalence to ff is equal to the application of the inverse of the time-slice map to ff: (timeSliceLinearEquivc)1(f)=(timeSlicec)1(f) (\text{timeSliceLinearEquiv}_c)^{-1}(f) = (\text{timeSlice}_c)^{-1}(f)

theorem

Action of the Distribution Time Slice on a Test Function

#distTimeSlice_apply

Let dd be the spatial dimension and MM be a real normed space. Given a speed of light cc, let ff be an MM-valued distribution on SpaceTime d\text{SpaceTime } d (a continuous linear map from S(SpaceTime d,R)\mathcal{S}(\text{SpaceTime } d, \mathbb{R}) to MM). For any Schwartz test function κS(Time×Space d,R)\kappa \in \mathcal{S}(\text{Time} \times \text{Space } d, \mathbb{R}), the action of the time-sliced distribution distTimeSlicecf\text{distTimeSlice}_c f on κ\kappa is given by: \[ (\text{distTimeSlice}_c f)(\kappa) = f(\kappa \circ \Phi_c) \] where Φc:SpaceTime dTime×Space d\Phi_c : \text{SpaceTime } d \to \text{Time} \times \text{Space } d is the continuous linear equivalence that identifies spacetime coordinates with time and space components according to cc.

theorem

((distTimeSlice c)1f)(κ)=f(κΦc1)((\text{distTimeSlice } c)^{-1} f)(\kappa) = f(\kappa \circ \Phi_c^{-1})

#distTimeSlice_symm_apply

Let cc be the speed of light. Let MM be a real normed space and dd be a natural number representing the spatial dimension. Given an MM-valued distribution ff on the product space Time×Spaced\text{Time} \times \text{Space}_d and a Schwartz test function κS(SpaceTimed,R)\kappa \in \mathcal{S}(\text{SpaceTime}_d, \mathbb{R}), the action of the inverse time-slice operator (distTimeSlice c)1(\text{distTimeSlice } c)^{-1} on ff evaluated at κ\kappa is given by: \[ ((\text{distTimeSlice } c)^{-1} f)(\kappa) = f(\kappa \circ \Phi_c^{-1}), \] where Φc1:Time×SpacedSpaceTimed\Phi_c^{-1}: \text{Time} \times \text{Space}_d \to \text{SpaceTime}_d is the inverse of the coordinate transformation map Φc:SpaceTimedTime×Spaced\Phi_c: \text{SpaceTime}_d \to \text{Time} \times \text{Space}_d defined by the speed of light cc.

theorem

distTimeSlicec(0f)=1ct(distTimeSlicecf)\text{distTimeSlice}_c (\partial_0 f) = \frac{1}{c} \partial_t (\text{distTimeSlice}_c f)

#distTimeSlice_distDeriv_inl

Let MM be a real normed space and dd be the spatial dimension. For a given speed of light cc, let ff be an MM-valued distribution on SpaceTime d\text{SpaceTime } d. Let distTimeSlicec\text{distTimeSlice}_c be the operator that transforms distributions on spacetime into distributions on the product space Time×Space d\text{Time} \times \text{Space } d. Let 0\partial_0 denote the distributional partial derivative with respect to the zeroth (temporal) coordinate index in spacetime, and let t\partial_t denote the physical time derivative operator on Time×Space d\text{Time} \times \text{Space } d. The theorem states that the time slice of the coordinate derivative is proportional to the physical time derivative of the time slice: \[ \text{distTimeSlice}_c (\partial_0 f) = \frac{1}{c} \frac{\partial}{\partial t} (\text{distTimeSlice}_c f) \]

theorem

0((distTimeSlice c)1f)=1c(distTimeSlice c)1(tf)\partial_0 ((\text{distTimeSlice } c)^{-1} f) = \frac{1}{c} (\text{distTimeSlice } c)^{-1} (\partial_t f)

#distDeriv_inl_distTimeSlice_symm

Let MM be a real normed space and dd be the spatial dimension. For a given speed of light cc, let ff be an MM-valued distribution on the product space Time×Space d\text{Time} \times \text{Space } d. Let (distTimeSlice c)1(\text{distTimeSlice } c)^{-1} denote the inverse time-slice operator that maps distributions on Time×Space d\text{Time} \times \text{Space } d back to distributions on SpaceTime d\text{SpaceTime } d. Let 0\partial_0 denote the distributional partial derivative with respect to the zeroth (temporal) coordinate index in spacetime, and let t\partial_t denote the physical time derivative operator on Time×Space d\text{Time} \times \text{Space } d. The theorem states that: \[ \partial_0 ((\text{distTimeSlice } c)^{-1} f) = \frac{1}{c} (\text{distTimeSlice } c)^{-1} \left( \frac{\partial f}{\partial t} \right) \]

theorem

(distTimeSlice c)1(tf)=c0((distTimeSlice c)1f)(\text{distTimeSlice } c)^{-1} (\partial_t f) = c \cdot \partial_0 ((\text{distTimeSlice } c)^{-1} f)

#distTimeSlice_symm_distTimeDeriv_eq

Let MM be a real normed space and dd be the spatial dimension. For a given speed of light cc, let ff be an MM-valued distribution on the product space Time×Space d\text{Time} \times \text{Space } d. Let (distTimeSlice c)1(\text{distTimeSlice } c)^{-1} denote the inverse time-slice operator that maps distributions on Time×Space d\text{Time} \times \text{Space } d back to distributions on SpaceTime d\text{SpaceTime } d. Let tf\partial_t f (or `Space.distTimeDeriv f`) denote the physical time derivative of the distribution on the product space, and let 0\partial_0 denote the distributional partial derivative with respect to the zeroth (temporal) coordinate index in spacetime. The theorem states that the inverse time-slice of the temporal derivative is equal to cc times the coordinate derivative of the inverse time-slice: \[ (\text{distTimeSlice } c)^{-1} \left( \frac{\partial f}{\partial t} \right) = c \cdot \partial_0 ((\text{distTimeSlice } c)^{-1} f) \]

theorem

distTimeSlicec\text{distTimeSlice}_c Commutes with Spatial Derivatives xi\frac{\partial}{\partial x_i}

#distTimeSlice_distDeriv_inr

Let dd be the spatial dimension, MM be a real normed vector space, and cc be the speed of light. Let f:SpaceTime dd[R]Mf: \text{SpaceTime } d \to d[\mathbb{R}] M be an MM-valued distribution on spacetime. For any spatial index i{0,,d1}i \in \{0, \dots, d-1\}, the time slice of the ii-th spatial partial derivative of ff is equal to the ii-th spatial partial derivative of the time-sliced distribution ff. That is, \[ \text{distTimeSlice}_c \left( \frac{\partial f}{\partial x_i} \right) = \frac{\partial}{\partial x_i} (\text{distTimeSlice}_c f) \] where on the left-hand side xi\frac{\partial}{\partial x_i} is the distributional derivative on SpaceTime d\text{SpaceTime } d, and on the right-hand side it is the distributional derivative on Time×Space d\text{Time} \times \text{Space } d.

theorem

distTimeSlicec1\text{distTimeSlice}_c^{-1} Commutes with Spatial Derivatives xi\frac{\partial}{\partial x_i}

#distDeriv_inr_distTimeSlice_symm

Let dd be the spatial dimension, MM be a real normed vector space, and cc be the speed of light. Let f:(Time×Space d)d[R]Mf: (\text{Time} \times \text{Space } d) \to d[\mathbb{R}] M be an MM-valued distribution. For any spatial index i{0,,d1}i \in \{0, \dots, d-1\}, the distributional spatial derivative of the inverse time-sliced distribution is equal to the inverse time-slice of the spatial derivative of ff. That is, \[ \partial_i (\text{distTimeSlice}_c^{-1} f) = \text{distTimeSlice}_c^{-1} \left( \frac{\partial f}{\partial x_i} \right) \] where on the left-hand side i\partial_i is the distributional derivative on SpaceTime d\text{SpaceTime } d, and on the right-hand side xi\frac{\partial}{\partial x_i} is the distributional derivative on Time×Space d\text{Time} \times \text{Space } d.