Physlib.SpaceAndTime.Space.Basic

For any dimension $d$, let $p$ and $q$ be points in the $d$-dimensional flat Euclidean space $\text{Space } d$. Let $p.\text{val}$ and $q.\text{val}$ denote their underlying coordinate representations (of type $\text{Fin } d \to \mathbb{R}$). Then, the two points are equal if and only if their coordinate representations are equal, that is, $p = q \iff p.\text{val} = q.\text{val}$.

For any dimension $d$, an element $p$ of the $d$-dimensional flat Euclidean space $\text{Space } d$ can be treated as a function mapping an index $i \in \{0, \dots, d-1\}$ to a real number $p_i \in \mathbb{R}$. This coercion allows a point in space to be evaluated at a specific coordinate index to retrieve its value.

For any dimension $d$, the $d$-dimensional flat Euclidean space $\text{Space } d$ is non-empty.

The $0$-dimensional flat Euclidean space $\text{Space } 0$ is a subsingleton. That is, for any two points $s_1, s_2 \in \text{Space } 0$, it holds that $s_1 = s_2$.

This instance defines the additive action of the Euclidean vector space $\mathbb{R}^d$ (modeled as `EuclideanSpace ℝ (Fin d)`) on the $d$-dimensional flat Euclidean space $\text{Space } d$. For a vector $v \in \text{EuclideanSpace } \mathbb{R}^d$ and a point $s \in \text{Space } d$, the translation $v +_{\text{v}} s$ results in a point whose coordinates are the sum of the components of $v$ and the coordinates of $s$, specifically $(v +_{\text{v}} s)_i = v_i + s_i$ for each index $i \in \{0, \dots, d-1\}$.

In $d$-dimensional flat Euclidean space ($\text{Space } d$), let $v$ be a vector in $\mathbb{R}^d$ (modeled as `EuclideanSpace ℝ (Fin d)`) and $s$ be a point in $\text{Space } d$. The coordinate representation of the point $v +_{\text{v}} s$, which is the result of translating $s$ by $v$, is the component-wise sum of the coordinates of $v$ and $s$. That is, for every index $i \in \{0, \dots, d-1\}$, $(v +_{\text{v}} s)_i = v_i + s_i$.

In a $d$-dimensional flat Euclidean space ($\text{Space } d$), let $v$ be a vector in $\mathbb{R}^d$ (represented by `EuclideanSpace ℝ (Fin d)`) and $s$ be a point in $\text{Space } d$. For any coordinate index $i \in \{0, \dots, d-1\}$, the $i$-th component of the point resulting from the translation of $s$ by $v$ (denoted $v +_{\text{v}} s$) is equal to the sum of the $i$-th component of $v$ and the $i$-th component of $s$. That is, $(v +_{\text{v}} s)_i = v_i + s_i$.

In $d$-dimensional flat Euclidean space ($\text{Space } d$), for any two points $s_1, s_2 \in \text{Space } d$, there exists a vector $v$ in the Euclidean vector space $\mathbb{R}^d$ (represented by `EuclideanSpace ℝ (Fin d)`) such that translating $s_1$ by $v$ results in $s_2$, denoted by $v +_{\text{v}} s_1 = s_2$.

This instance defines the additive action of the $d$-dimensional Euclidean vector space $\mathbb{R}^d$ (represented by `EuclideanSpace ℝ (Fin d)`) on the flat Euclidean space $\text{Space } d$. This action represents translation, ensuring that for any point $s \in \text{Space } d$ and any vectors $v, v_1, v_2 \in \mathbb{R}^d$, the following axioms of an additive group action are satisfied: 1. The zero vector acts as the identity: $0 +_{\text{v}} s = s$. 2. The action is compatible with vector addition: $(v_1 + v_2) +_{\text{v}} s = v_1 +_{\text{v}} (v_2 +_{\text{v}} s)$.

For a $d$-dimensional flat Euclidean space $\text{Space } d$, this definition provides the vector subtraction (displacement) operation $\ominus$ (represented by the `VSub` typeclass). Given two points $s_1, s_2 \in \text{Space } d$, the result $s_1 -_v s_2$ is a displacement vector in the Euclidean space $\mathbb{R}^d$ (specifically `EuclideanSpace ℝ (Fin d)` with the $L^2$ norm) whose components are defined by $(s_1 -_v s_2)_i = s_1(i) - s_2(i)$ for each coordinate index $i \in \{0, \dots, d-1\}$.

In the $d$-dimensional flat Euclidean space $\text{Space } d$, for any two points $s_1, s_2 \in \text{Space } d$ and any coordinate index $i \in \{0, \dots, d-1\}$, the $i$-th component of the displacement vector $s_1 -_v s_2$ is equal to the difference between the $i$-th coordinates of $s_1$ and $s_2$: $$(s_1 -_v s_2)_i = s_1(i) - s_2(i)$$ Here, the subtraction $s_1 -_v s_2$ (provided by the `VSub` instance) represents the vector in $\mathbb{R}^d$ pointing from $s_2$ to $s_1$.

The $d$-dimensional flat Euclidean space $\text{Space } d$ is an additive torsor (or affine space) modeled on the Euclidean vector space $\mathbb{R}^d$ (specifically `EuclideanSpace ℝ (Fin d)`). This structure provides a free and transitive additive action of vectors in $\mathbb{R}^d$ on points in $\text{Space } d$, representing translations. It ensures that for any points $s_1, s_2, s \in \text{Space } d$ and any vector $v \in \mathbb{R}^d$, the following identities hold: 1. $(s_1 -_v s_2) +_v s_2 = s_1$ 2. $(v +_v s) -_v s = v$ where $+_v$ denotes the translation of a point by a vector and $-_v$ denotes the displacement vector between two points.

For any two points $p, q$ in the $d$-dimensional flat Euclidean space $\text{Space } d$, the distance function $\text{dist}(p, q)$ is defined as the Euclidean distance: $$\text{dist}(p, q) = \sqrt{\sum_{i=0}^{d-1} (p_i - q_i)^2}$$ where $p_i$ and $q_i$ denote the $i$-th coordinates of the points $p$ and $q$ respectively.

For any two points $p$ and $q$ in the $d$-dimensional flat Euclidean space $\text{Space } d$, the distance between them is given by the square root of the sum of the squared differences of their coordinates: $$\text{dist}(p, q) = \sqrt{\sum_{i} (p_i - q_i)^2}$$ where $p_i$ and $q_i$ denote the $i$-th coordinates of the points $p$ and $q$ respectively, and the sum ranges over all indices $i \in \{0, \dots, d-1\}$.

The $d$-dimensional flat Euclidean space $\text{Space } d$ is equipped with a pseudo-metric space structure. The distance between any two points $p, q \in \text{Space } d$ is defined by the Euclidean metric: $$\text{dist}(p, q) = \sqrt{\sum_{i=0}^{d-1} (p_i - q_i)^2}$$ This structure satisfies the axioms of a pseudo-metric space, including the property that $\text{dist}(p, p) = 0$, symmetry $\text{dist}(p, q) = \text{dist}(q, p)$, and the triangle inequality $\text{dist}(p, r) \leq \text{dist}(p, q) + \text{dist}(q, r)$.

The $d$-dimensional flat Euclidean space $\text{Space } d$ is a normed additive torsor (or normed affine space) modeled on the Euclidean vector space $\mathbb{R}^d$ (specifically `EuclideanSpace ℝ (Fin d)`). This structure identifies the distance between any two points $p, q \in \text{Space } d$ with the Euclidean norm of their displacement vector $p - q \in \mathbb{R}^d$: $$\text{dist}(p, q) = \|p - q\|$$ where $\|\cdot\|$ denotes the standard Euclidean norm $\sqrt{\sum p_i^2}$.

The $d$-dimensional flat Euclidean space $\text{Space } d$ is equipped with a metric space structure. This structure defines a distance function $\text{dist}(p, q)$ for any two points $p, q \in \text{Space } d$ using the standard Euclidean metric: $$\text{dist}(p, q) = \sqrt{\sum_{i=0}^{d-1} (p_i - q_i)^2}$$ As a metric space, it satisfies the identity of indiscernibles, meaning that $\text{dist}(p, q) = 0$ if and only if $p = q$, in addition to the properties of a pseudo-metric space (symmetry and the triangle inequality).

For any natural number $d$, the $(d+1)$-dimensional flat Euclidean space $\text{Space}(d+1)$ is nontrivial, meaning it contains at least two distinct points.

The manifold structure on the $d$-dimensional flat Euclidean space $\text{Space } d$ is established by modeling it on the Euclidean vector space $\mathbb{R}^d$. This structure is defined via a global coordinate chart that identifies the affine space $\text{Space } d$ with $\mathbb{R}^d$ by choosing an arbitrary origin $p_0 \in \text{Space } d$ and mapping each point $s \in \text{Space } d$ to the displacement vector $s - p_0 \in \mathbb{R}^d$.

For any natural number $d$, let $I$ be the map defining the manifold structure on the $d$-dimensional flat Euclidean space $\text{Space } d$, which identifies it with the model space $\mathbb{R}^d$. The composition of $I$ and its inverse $I^{-1}$ is the identity function on $\mathbb{R}^d$, i.e., $I \circ I^{-1} = \text{id}$.

Let $\phi$ be the manifold structure map (the global coordinate chart) that identifies the $d$-dimensional flat Euclidean space $\text{Space } d$ with the Euclidean vector space $\mathbb{R}^d$. For any vector $x \in \mathbb{R}^d$, applying the map $\phi$ to the image of $x$ under the inverse mapping $\phi^{-1}$ returns the original vector $x$: $$\phi(\phi^{-1}(x)) = x$$

Let $I$ be the map defining the manifold structure on the $d$-dimensional flat Euclidean space $\text{Space } d$, which identifies it with the Euclidean model space $\mathbb{R}^d$. The range of $I$ is the entire model space $\mathbb{R}^d$: $$\text{range}(I) = \mathbb{R}^d$$

For any natural number $d$, the map $\phi: \text{Space } d \to \mathbb{R}^d$ that defines the manifold structure on the $d$-dimensional flat Euclidean space is infinitely differentiable, i.e., it is of class $C^\infty$. This map $\phi$ corresponds to the global coordinate chart that identifies points in the space with their coordinates in the model Euclidean vector space $\mathbb{R}^d$.