Physlib.SpaceAndTime.SpaceTime.Basic

For a given dimension $d \in \mathbb{N}$ and an index $\mu \in \{0, \dots, d\}$, the function $\text{coord}(\mu)$ is the linear map from the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ to the real numbers $\mathbb{R}$ that extracts the $\mu$-th coordinate of a spacetime vector $p$. This map is also denoted by $\mathfrak{x}_\mu(p)$.

The notation $\mathfrak{x}$ is defined as an alias for the coordinate function `coord`. For a given dimension $d$ and an index $\mu \in \{0, \dots, d\}$, $\mathfrak{x}(\mu)$ represents the linear map from the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ to the real numbers $\mathbb{R}$ that extracts the $\mu$-th component of a spacetime vector.

In a $(d+1)$-dimensional spacetime, for any vector $y \in \text{SpaceTime } d$ and any index $\mu \in \{0, \dots, d\}$, the value of the spacetime coordinate map $\mathfrak{x}_\mu(y)$ is equal to the value of the vector $y$ at the index corresponding to $\mu$. This correspondence is defined by the equivalence between the index set $\text{Fin}(1+d)$ and the sum of time and space indices $\text{Fin } 1 \oplus \text{Fin } d$.

For a spatial dimension $d$ and a coordinate index $\mu \in \text{Fin } 1 \oplus \text{Fin } d$, this definition provides the continuous linear map from the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ to the real numbers $\mathbb{R}$ that maps a spacetime vector $x$ to its $\mu$-th coordinate value $x_\mu$.

For any $d \in \mathbb{N}$, the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is equipped with a measurable space structure defined by the Borel $\sigma$-algebra, which is the $\sigma$-algebra generated by the open sets of its underlying topology.

For any $d \in \mathbb{N}$, the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is a Borel space, meaning that its measurable space structure is defined by the Borel $\sigma$-algebra generated by the open sets of its topology.

For any $d \in \mathbb{N}$, the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is equipped with a measure space structure. The volume measure on this space is defined as the additive Haar measure induced by the standard coordinate basis of the underlying Lorentz vector space $\text{Vector}_d$.

For any natural number $d$, the volume measure on the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is strictly positive on every non-empty open set.

For any natural number $d$, the volume measure on the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is finite on every compact set.

For any natural number $d$, the canonical volume measure on the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ is an additive Haar measure.

For any $d \in \mathbb{N}$, the map $\text{space} : \text{SpaceTime } d \to \text{Space } d$ is a continuous linear map over $\mathbb{R}$ that extracts the spatial component of a spacetime vector. For a vector $x \in \text{SpaceTime } d$, this function returns its spatial part $\vec{x} \in \text{Space } d$, which corresponds to the components indexed by the spatial dimensions.

For any natural number $d$ and any spacetime vector $f \in \text{SpaceTime } d$ represented by its coordinate function $f: \text{Fin } 1 \oplus \text{Fin } d \to \mathbb{R}$, the spatial projection $\text{space}(f)$ is the vector in $\text{Space } d$ whose components are given by the spatial entries of $f$. Specifically, $(\text{space}(f))_i = f(\text{inr } i)$ for each spatial index $i \in \text{Fin } d$, where $\text{inr}$ embeds the spatial indices into the full spacetime coordinate set.

The spatial projection map $\text{space} : \text{SpaceTime } d \to \text{Space } d$ is equivariant with respect to rotations. That is, for any rotation $R$ and any spacetime vector $x \in \text{SpaceTime } d$, the spatial component of the rotated vector is the rotation of the spatial component: $\text{space}(R \cdot x) = R \cdot \text{space}(x)$.

For any natural number $d$, representing the spatial dimension, and any speed of light $c$, let $f : \text{Fin } 1 \oplus \text{Fin } d \to \mathbb{R}$ be a function representing the coordinates of a spacetime vector in $d+1$ dimensions. The value of the temporal component of $f$, denoted as $(\text{time}_c f).\text{val}$, is given by the coordinate at the temporal index divided by the speed of light: $$(\text{time}_c f).\text{val} = \frac{f(\text{inl } 0)}{c}$$ where $\text{inl } 0$ denotes the index corresponding to the temporal dimension.

For any spatial dimension $d \in \mathbb{N}$ and speed of light $c$, let $x$ be a vector in the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$. Let $x.\text{time}(c)$ and $x.\text{space}$ denote the temporal and spatial components of $x$, respectively. Then, the inverse of the continuous linear equivalence $\text{toTimeAndSpace}_c$ (which maps spacetime vectors to the product space $\text{Time} \times \text{Space } d$) applied to these components recovers the original vector: $$(\text{toTimeAndSpace}_c)^{-1}(x.\text{time}(c), x.\text{space}) = x$$

For any spatial dimension $d \in \mathbb{N}$ and speed of light $c$, let $\text{toTimeAndSpace}_c$ be the continuous linear equivalence that maps a spacetime vector in $\text{SpaceTime } d$ to its temporal and spatial components in $\text{Time} \times \text{Space } d$. For any time $t \in \text{Time}$ and spatial position $s \in \text{Space } d$, the spatial projection $(\cdot).\text{space}$ of the spacetime vector reconstructed from $(t, s)$ via the inverse map $(\text{toTimeAndSpace}_c)^{-1}$ is equal to $s$: $$((\text{toTimeAndSpace}_c)^{-1}(t, s)).\text{space} = s$$

For any spatial dimension $d \in \mathbb{N}$ and speed of light $c$, let $\Phi_c : \text{SpaceTime } d \cong \text{Time} \times \text{Space } d$ be the continuous linear equivalence (the map `toTimeAndSpace c`) that decomposes a spacetime vector into its temporal and spatial parts. For any time $t \in \text{Time}$ and spatial point $s \in \text{Space } d$, the temporal component of the spacetime vector reconstructed from the pair $(t, s)$ via the inverse mapping $\Phi_c^{-1}$ is equal to $t$: $$(\Phi_c^{-1}(t, s)).\text{time}(c) = t$$

Given a spatial dimension $d$, a speed of light $c$, a time $t \in \text{Time}$, and a spatial point $s \in \text{Space } d$, the $0$-th component (the temporal index) of the spacetime vector mapped from the coordinates $(t, s)$ via the inverse of the linear equivalence $\text{toTimeAndSpace}(c)$ is equal to $c \cdot t$.

Given a spatial dimension $d$ and speed of light $c$, let $\Phi_c: \text{SpaceTime } d \cong \text{Time} \times \text{Space } d$ be the continuous linear equivalence between spacetime and its time-space decomposition. For any time $t \in \text{Time}$, spatial vector $x \in \text{Space } d$, and spatial index $i \in \{0, \dots, d-1\}$, the value of the reconstructed spacetime vector $\Phi_c^{-1}(t, x)$ at the index $i$ of its spatial part is equal to the $i$-th component of the vector $x$, denoted $x_i$.

For any spatial dimension $d \in \mathbb{N}$ and speed of light $c$, let $\Phi_c : \text{SpaceTime } d \cong \text{Time} \times \text{Space } d$ be the continuous linear equivalence `toTimeAndSpace`. For any point $x \in \text{SpaceTime } d$, the Fréchet derivative of $\Phi_c$ at $x$ with respect to the real numbers $\mathbb{R}$ is equal to the underlying continuous linear map of $\Phi_c$.

Let $d$ be a natural number and $c$ be the speed of light. Let $\Phi_c : \text{SpaceTime } d \cong \text{Time} \times \text{Space } d$ be the continuous linear equivalence `toTimeAndSpace c`. For any point $x \in \text{Time} \times \text{Space } d$, the Fréchet derivative of the inverse map $\Phi_c^{-1}$ at $x$ is equal to the continuous linear map underlying $\Phi_c^{-1}$.

For any spatial dimension $d \in \mathbb{N}$, speed of light $c$, and spatial index $i \in \{0, 1, \dots, d-1\}$, the continuous linear equivalence $\text{toTimeAndSpace } c$ maps the $i$-th spatial basis vector of $\text{SpaceTime } d$ (denoted by the index $\text{inr } i$) to the pair $(0, \text{basis}_i)$, where $0 \in \text{Time}$ and $\text{basis}_i$ is the $i$-th vector of the standard orthonormal basis of $\text{Space } d$.

For any spatial dimension $d$ and speed of light $c$, the continuous linear equivalence $\text{toTimeAndSpace}_c: \text{SpaceTime } d \to \text{Time} \times \text{Space } d$ maps the temporal basis vector $\mathbf{e}_0$ (the basis vector of the underlying Lorentz vector space indexed by the temporal dimension) to the pair $(1/c, \mathbf{0})$, where $1/c \in \text{Time}$ and $\mathbf{0} \in \text{Space } d$.

For any spatial dimension $d$ and speed of light $c$, the continuous linear equivalence $\text{toTimeAndSpace}_c : \text{SpaceTime } d \to \text{Time} \times \text{Space } d$ maps the temporal basis vector $\mathbf{e}_0$ to the scalar product $\frac{1}{c} \cdot (1, \mathbf{0})$, where $1 \in \text{Time}$ and $\mathbf{0} \in \text{Space } d$.

For any spatial dimension $d \in \mathbb{N}$ and speed of light $c$, the basis vector of the time-space basis $\text{timeSpaceBasis}_c$ corresponding to the temporal index (denoted by $\text{Sum.inl } 0$) is equal to the numerical value of $c$ multiplied by the temporal basis vector $\mathbf{e}_0$ of the standard Lorentz basis $\text{Lorentz.Vector.basis}$.

For any spatial dimension $d \in \mathbb{N}$, speed of light $c$, and spatial index $i \in \{0, 1, \dots, d-1\}$, the $i$-th spatial vector of the time-space basis for $(d+1)$-dimensional spacetime (indexed by $\text{inr } i$) is equal to the $i$-th spatial vector of the standard Lorentz basis.

For a spatial dimension $d \in \mathbb{N}$ and a speed of light $c$, this defines a continuous linear equivalence $f: \text{SpaceTime}_d \simeq_{L}[\mathbb{R}] \text{SpaceTime}_d$. The map scales the temporal component of a spacetime vector by $c$ while leaving the spatial components unchanged. Specifically, for a vector $x \in \text{SpaceTime}_d$, the component $x_0$ (corresponding to the temporal index) is mapped to $c \cdot x_0$, and the components $x_i$ (for spatial indices $i \in \{1, \dots, d\}$) remain the same.

For any spatial dimension $d$ and speed of light $c$, the determinant of the continuous linear equivalence $\text{timeSpaceBasisEquiv}_c$ on $(d+1)$-dimensional spacetime—which scales the temporal component of a vector by $c$ while leaving the $d$ spatial components unchanged—is equal to the value of $c$.

For a given spatial dimension $d \in \mathbb{N}$ and speed of light $c$, the basis $\text{timeSpaceBasis}_c$ for the $(d+1)$-dimensional spacetime $\text{SpaceTime}_d$ is equal to the basis obtained by applying the linear equivalence $\text{timeSpaceBasisEquiv}_c$ to the standard Lorentz basis. This equivalence is the map that scales the temporal component of a vector by the value of $c$ and leaves the spatial components unchanged.

For any spatial dimension $d$ and speed of light $c$, let $\Phi_c : \text{SpaceTime}_d \to \text{Time} \times \text{Space}_d$ be the continuous linear equivalence that maps a spacetime vector to its temporal and spatial components. Its inverse map, $\Phi_c^{-1}$, is measure-preserving from the product volume measure on $\text{Time} \times \text{Space}_d$ to the volume measure on $\text{SpaceTime}_d$ scaled by a factor of $c^{-1}$.

For a given spatial dimension $d$ and speed of light $c$, let $f: \text{SpaceTime } d \to M$ be a function mapping into a real normed space $M$. The integral of $f$ over the $(d+1)$-dimensional spacetime $\text{SpaceTime } d$ with respect to its volume measure is equal to $c$ times the integral of the composition of $f$ with the inverse of the time-space decomposition map over the product space $\text{Time} \times \text{Space } d$: $$\int_{\text{SpaceTime } d} f(x) \, dx = c \int_{\text{Time} \times \text{Space } d} f((\text{toTimeAndSpace } c)^{-1}(t, \mathbf{x})) \, d(t, \mathbf{x})$$ where $\text{toTimeAndSpace } c$ is the continuous linear equivalence that decomposes a spacetime vector into its temporal and spatial components, and the right-hand side is integrated with respect to the product measure of the volumes on $\text{Time}$ and $\text{Space } d$.

For a given spatial dimension $d$ and speed of light $c$, let $\Phi_c : \text{SpaceTime}_d \to \text{Time} \times \text{Space}_d$ be the continuous linear equivalence that decomposes a spacetime vector into its temporal and spatial components. For any function $f: \text{SpaceTime}_d \to M$ mapping into a normed additive commutative group $M$, $f$ is integrable with respect to the volume measure on $\text{SpaceTime}_d$ if and only if the composition $f \circ \Phi_c^{-1}$ is integrable with respect to the product volume measure on $\text{Time} \times \text{Space}_d$.

For a given spatial dimension $d$ and speed of light $c$, let $f: \text{SpaceTime}_d \to M$ be a function mapping into a real normed space $M$. If $f$ is integrable with respect to the volume measure on $\text{SpaceTime}_d$, then its integral is equal to $c$ times the iterated integral over $\text{Time}$ and $\text{Space}_d$: $$\int_{\text{SpaceTime}_d} f(x) \, dx = c \int_{\text{Time}} \left( \int_{\text{Space}_d} f(\Phi_c^{-1}(t, \mathbf{x})) \, d\mathbf{x} \right) dt$$ where $\Phi_c: \text{SpaceTime}_d \to \text{Time} \times \text{Space}_d$ is the continuous linear equivalence that decomposes a spacetime vector into its temporal and spatial components.

For a spatial dimension $d$ and speed of light $c$, let $f: \text{SpaceTime}_d \to M$ be an integrable function mapping into a real normed space $M$. Let $\Phi_c : \text{SpaceTime}_d \to \text{Time} \times \text{Space}_d$ be the continuous linear equivalence that decomposes a spacetime vector into its temporal and spatial components. The integral of $f$ over the $(d+1)$-dimensional spacetime with respect to its volume measure is equal to the speed of light $c$ multiplied by the iterated integral of $f \circ \Phi_c^{-1}$ over $\text{Space}_d$ and then over $\text{Time}$: $$\int_{\text{SpaceTime}_d} f(x) \, dx = c \int_{\text{Space}_d} \int_{\text{Time}} f(\Phi_c^{-1}(t, \mathbf{x})) \, dt \, d\mathbf{x}$$