Physlib.SpaceAndTime.Space.Module

For a given dimension $d$, the addition operation on $\text{Space } d$ is defined such that for any two elements $p, q \in \text{Space } d$, their sum $p + q$ is the element whose components are given by the sum of the corresponding components of $p$ and $q$. That is, for each index $i$, $(p + q)_i = p_i + q_i$.

For any natural number $d$ and any elements $x, y \in \text{Space } d$, the underlying vector value of their sum is equal to the sum of their individual underlying vector values. This is expressed as $(x + y).\text{val} = x.\text{val} + y.\text{val}$.

For any dimension $d \in \mathbb{N}$, given two elements $x, y \in \text{Space } d$ and an index $i \in \{0, \dots, d-1\}$, the $i$-th coordinate of their sum $x + y$ is equal to the sum of their individual $i$-th coordinates. That is, $(x + y)_i = x_i + y_i$.

For any dimension $d$, the zero element $0 \in \text{Space } d$ is defined as the element whose components are all equal to $0$.

For any dimension $d \in \mathbb{N}$, the underlying value of the zero element $0 \in \text{Space } d$ is the constant function that maps every index to $0$.

For any natural number $d$ and any index $i \in \{0, \dots, d-1\}$, the $i$-th component of the zero element $0 \in \text{Space } d$ is equal to $0$.

For a given dimension $d$, the type $\text{Space } d$ is equipped with the structure of an additive commutative monoid. This means that for all elements $a, b, c \in \text{Space } d$, the addition operation is associative, $(a + b) + c = a + (b + c)$, and commutative, $a + b = b + a$. Furthermore, the zero element $0 \in \text{Space } d$ acts as the additive identity, satisfying $0 + a = a$ and $a + 0 = a$.

For any dimension $d \in \mathbb{N}$, natural number $n \in \mathbb{N}$, and element $a \in \text{Space } d$, the underlying representation of the natural scalar multiplication $n \cdot a$ is the function that maps each index $i \in \{0, \dots, d-1\}$ to the scalar product $n \cdot a_i$, where $a_i$ denotes the $i$-th component of $a$.

For any dimension $d \in \mathbb{N}$, any natural number $n \in \mathbb{N}$, any element $a \in \text{Space } d$, and any index $i \in \{0, \dots, d-1\}$, the $i$-th component of the natural scalar multiplication $n \cdot a$ is equal to the natural scalar multiplication of $n$ with the $i$-th component of $a$. This is expressed by the identity $(n \cdot a)_i = n \cdot a_i$.

For any dimension $d \in \mathbb{N}$ and any two vectors $v_1, v_2$ in the Euclidean space $\mathbb{R}^d$, let $0$ denote the zero element of $\text{Space } d$. The sum of the points $v_1 +_{\text{v}} 0$ and $v_2 +_{\text{v}} 0$ in $\text{Space } d$ is equal to the point $(v_1 + v_2) +_{\text{v}} 0$, where $+_{\text{v}}$ denotes the additive action of a vector on a point. That is, $$(v_1 +_{\text{v}} 0) + (v_2 +_{\text{v}} 0) = (v_1 + v_2) +_{\text{v}} 0.$$

The definition provides a scalar multiplication operation of real numbers $c \in \mathbb{R}$ on elements $p$ of the $d$-dimensional space $\text{Space } d$. For any scalar $c$ and point $p$, the result $c \cdot p$ is defined component-wise such that its $i$-th coordinate is the product of $c$ and the $i$-th coordinate of $p$, i.e., $(c \cdot p)_i = c \cdot p_i$ for all $i \in \{1, \dots, d\}$.

For any natural number $d$, real scalar $c \in \mathbb{R}$, and point $p \in \text{Space } d$, the coordinate-wise representation of the scalar product $c \cdot p$ is given by the function mapping each index $i$ to the product of $c$ and the $i$-th coordinate of $p$. That is, $(c \cdot p).\text{val}(i) = c \cdot p.\text{val}(i)$.

For any natural number $d$, real number $c$, and point $p \in \text{Space } d$, the $i$-th coordinate of the scalar product $c \cdot p$ is equal to the product of $c$ and the $i$-th coordinate of $p$, i.e., $(c \cdot p)_i = c \cdot p_i$ for all indices $i \in \{0, \dots, d-1\}$.

For any dimension $d$, real scalar $k \in \mathbb{R}$, and vector $v$ in the $d$-dimensional Euclidean space $\text{EuclideanSpace } \mathbb{R}^d$, the scalar multiplication of the point $v +_v 0$ by $k$ is equal to the translation of the origin $0 \in \text{Space } d$ by the scaled vector $k \cdot v$. That is, \[ k \cdot (v +_v 0) = (k \cdot v) +_v 0 \] where $0$ is the zero element of $\text{Space } d$ and $+_v$ denotes the operation of adding a vector to a point.

For a natural number $d$, the type $\text{Space } d$ is equipped with the structure of a module over the real numbers $\mathbb{R}$. This defines $\text{Space } d$ as a real vector space where the scalar multiplication $c \cdot p$ and addition $p_1 + p_2$ satisfy the standard axioms (associativity, distributivity, and identity) through component-wise operations.

The Euclidean norm $\|p\|$ for an element $p$ in the $d$-dimensional space $\text{Space } d$ is defined as the square root of the sum of the squares of its components: \[ \|p\| = \sqrt{\sum_{i} (p_i)^2} \] where $p_i$ denotes the $i$-th coordinate of $p$.

For an element $p$ in the $d$-dimensional space $\text{Space } d$, the Euclidean norm $\|p\|$ is equal to the square root of the sum of the squares of its coordinates $p_i$: \[ \|p\| = \sqrt{\sum_{i} (p_i)^2} \]

For any element $p$ in the $d$-dimensional space $\text{Space } d$ and any coordinate index $i \in \{0, \dots, d-1\}$, the absolute value of the $i$-th coordinate $p_i$ is less than or equal to the Euclidean norm $\|p\|$ of the element: \[ |p_i| \le \|p\| \]

For any element $p$ in the $d$-dimensional space $\text{Space } d$, the square of its Euclidean norm $\|p\|^2$ is equal to the sum of the squares of its coordinates $p_i$: \[ \|p\|^2 = \sum_{i} p_i^2 \] where $p_i$ denotes the $i$-th coordinate of $p$.

In the zero-dimensional space $\text{Space } 0$, any element $p$ is equal to the zero element $0$.

For any dimension $d$ and any vector $v$ in the $d$-dimensional Euclidean space $\mathbb{R}^d$ (represented as `EuclideanSpace ℝ (Fin d)`), the norm of the element in $\text{Space } d$ obtained by adding the vector $v$ to the zero element $0$ is equal to the norm of $v$: \[ \|v +_{\text{v}} 0\| = \|v\| \] where $+_{\text{v}}$ denotes the additive action of a vector on a point.

For any element $p$ in the $d$-dimensional space $\text{Space } d$, the negation $-p$ is defined component-wise such that for each index $i \in \{1, \dots, d\}$, the $i$-th component of the result is $(-p)_i = -p_i$.

For any element $p$ in the $d$-dimensional space $\text{Space } d$, the valuation of its negation $-p$ is obtained by negating each component of $p$. Mathematically, for every index $i \in \{0, \dots, d-1\}$, the $i$-th component of the negation is given by $(-p)_i = -p_i$.

For any natural number $d$, any vector $p$ in the $d$-dimensional space $\text{Space } d$, and any index $i \in \{0, \dots, d-1\}$, the $i$-th component of the negation of $p$ is equal to the negative of its $i$-th component, i.e., $(-p)_i = -p_i$.

For any dimension $d$, the type $\text{Space } d$ is equipped with the structure of an additive commutative group. This means that for all elements $p, q, r \in \text{Space } d$, the addition operation is associative, $(p + q) + r = p + (q + r)$, and commutative, $p + q = q + p$. There exists a zero element $0$ such that $p + 0 = p$, and for every element $p$, there exists an additive inverse $-p$ such that $p + (-p) = 0$. Additionally, integer scalar multiplication $z \cdot p$ for $z \in \mathbb{Z}$ is defined component-wise such that $(z \cdot p)_i = z \cdot p_i$ for each index $i$.

For any dimension $d \in \mathbb{N}$, given two elements $p, q \in \text{Space } d$ and an index $i \in \{0, \dots, d-1\}$, the $i$-th coordinate of their difference $p - q$ is equal to the difference of their individual $i$-th coordinates. That is, $(p - q)_i = p_i - q_i$.

For any dimension $d$ and any two elements $p, q \in \text{Space } d$, the value function of their difference $p - q$ is equal to the pointwise difference of their respective value functions. Specifically, for every index $i \in \{0, \dots, d-1\}$, the $i$-th component of the difference satisfies $(p - q)_i = p_i - q_i$.

For any dimension $d$ and any two vectors $v_1, v_2 \in \mathbb{R}^d$, the following identity holds in $\text{Space } d$: \[ (v_1 + 0) - (v_2 + 0) = (v_1 - v_2) + 0 \] where $0$ is the zero element of $\text{Space } d$, $+$ denotes the additive action of a vector on a point, and $-$ denotes the subtraction operation within the additive group structure of $\text{Space } d$.

For any dimension $d$ and points $p, q$ in the $d$-dimensional space $\text{Space } d$, the distance between $p$ and $q$ is equal to the norm of their difference: \[ \text{dist}(p, q) = \|p - q\| \] where $\| \cdot \|$ denotes the Euclidean norm on $\text{Space } d$.

For any dimension $d$, the space $\text{Space } d$ is equipped with the structure of a seminormed additive commutative group. This structure ensures that $\text{Space } d$ is an additive commutative group where the distance between any two points $p$ and $q$ is induced by the norm of their difference, such that $\text{dist}(p, q) = \|p - q\|$.

For any dimension $d$, the space $\text{Space } d$ is equipped with the structure of a normed additive commutative group. This structure combines its additive commutative group properties with a norm $\|\cdot\|$ such that the distance between any two points $x, y \in \text{Space } d$ is induced by the norm of their difference: \[ \text{dist}(x, y) = \|x - y\| \] where the norm is the Euclidean norm defined as $\|p\| = \sqrt{\sum_{i} (p_i)^2}$.

The definition provides an inner product structure on the $d$-dimensional space `Space d` over the real numbers $\mathbb{R}$. For any two elements $p, q \in \text{Space}_d$, their inner product is defined as the sum of the products of their components: $$\langle p, q \rangle = \sum_{i} p_i q_i$$

For any dimension $d$ and any two vectors $v_1, v_2$ in the Euclidean space $\mathbb{R}^d$, let $0$ denote the zero element of $\text{Space}_d$. The inner product of the points $v_1 +_v 0$ and $v_2 +_v 0$ in $\text{Space}_d$ is equal to the Euclidean inner product of $v_1$ and $v_2$: $$\langle v_1 +_v 0, v_2 +_v 0 \rangle = \langle v_1, v_2 \rangle$$ where $+_v$ denotes the action of a vector on a point in the space.

In the $d$-dimensional space $Space(d)$, the inner product of any two elements $p, q \in Space(d)$ is equal to the sum of the products of their components: $$\langle p, q \rangle = \sum_{i} p_i q_i$$

For any dimension $d$, the space $\text{Space } d$ is equipped with the structure of an inner product space over the real numbers $\mathbb{R}$. The inner product for elements $p, q \in \text{Space } d$ is defined as the sum of the products of their components, $\langle p, q \rangle = \sum_{i} p_i q_i$, which induces the corresponding norm and metric properties on the space.

For a space of dimension $d$ (denoted by $Space(d)$), the measurable space structure is defined as the Borel $\sigma$-algebra, which is the $\sigma$-algebra generated by the open sets of its topology.

For any natural number $d$, the $d$-dimensional space $\text{Space}(d)$ is a Borel space, meaning that its measurable space structure is defined by the Borel $\sigma$-algebra, which is the $\sigma$-algebra generated by the open sets of its topology.

For any dimension $d$ and any two vectors $p, q$ in the $d$-dimensional space $\text{Space}_d$, the inner product of $p$ and $q$ is equal to the sum of the products of their corresponding components: $$\langle p, q \rangle = \sum_i p_i q_i$$ where $p_i$ and $q_i$ denote the $i$-th components of the vectors $p$ and $q$.

For any dimension $d \in \mathbb{N}$, finite index set $\iota$, and family of vectors $f : \iota \to \text{Space } d$, the $i$-th coordinate of the sum of the vectors is equal to the sum of the $i$-th coordinates of each vector. That is, for any index $i \in \{0, \dots, d-1\}$: $$\left( \sum_{x \in \iota} f(x) \right)_i = \sum_{x \in \iota} f(x)_i$$

For any dimension $d$, the standard basis of $\text{Space } d$ is an orthonormal basis indexed by the set $\{0, 1, \dots, d-1\}$. This basis provides an isometric isomorphism between the real inner product space $\text{Space } d$ and $\mathbb{R}^d$, such that the coordinate representation of a vector $p$ is given by its components $p_i$, preserving the Euclidean ($L^2$) norm.

For any dimension $d$, vector $p \in \text{Space } d$, and index $i \in \{0, 1, \dots, d-1\}$, the $i$-th coordinate of $p$ is equal to the $i$-th component of the representation of $p$ with respect to the standard orthonormal basis of $\text{Space } d$.

For any dimension $d$, given a vector $p$ in the real inner product space $\text{Space } d$ and an index $i \in \{0, 1, \dots, d-1\}$, the $i$-th component of the coordinate representation of $p$ with respect to the standard orthonormal basis is equal to the $i$-th coordinate of $p$. That is, \[ (\text{basis.repr } p)_i = p_i \] where $\text{basis.repr}$ is the isometric isomorphism between $\text{Space } d$ and the Euclidean space $\mathbb{R}^d$ provided by the standard basis.

For any dimension $d$, given a vector $v$ in the Euclidean space $\mathbb{R}^d$ and an index $i \in \{0, 1, \dots, d-1\}$, the $i$-th component of the element in $\text{Space } d$ obtained by the inverse coordinate representation map $\text{basis.repr}^{-1}$ applied to $v$ is equal to the $i$-th component of $v$. That is, \[ (\text{basis.repr}^{-1}(v))_i = v_i \] where $\text{basis.repr}$ is the isometric isomorphism between $\text{Space } d$ and $\mathbb{R}^d$ provided by the standard orthonormal basis.

For any dimension $d$ and indices $i, j \in \{0, 1, \dots, d-1\}$, the $j$-th component of the $i$-th vector in the standard orthonormal basis of $\text{Space } d$ is equal to 1 if $i = j$ and 0 otherwise. In other words, $(\text{basis}_i)_j = \delta_{ij}$, where $\delta_{ij}$ is the Kronecker delta.

For any dimension $d$ and index $i \in \{0, 1, \dots, d-1\}$, the $i$-th component of the $i$-th vector in the standard orthonormal basis of $\text{Space } d$ is equal to 1. That is, $(\text{basis}_i)_i = 1$.

For any dimension $d$, let $p$ be a vector in the $d$-dimensional real inner product space $\text{Space } d$. For any index $i \in \{0, 1, \dots, d-1\}$, the inner product of $p$ with the $i$-th vector of the standard orthonormal basis is equal to the $i$-th component of $p$: $$\langle p, \text{basis}_i \rangle = p_i$$

For any dimension $d$, given an index $i \in \{0, 1, \dots, d-1\}$ and a vector $p$ in the $d$-dimensional real inner product space $\text{Space } d$, the inner product of the $i$-th standard orthonormal basis vector with $p$ is equal to the $i$-th component of $p$: $$\langle \text{basis}_i, p \rangle = p_i$$

Let $\text{Space } d$ be the $d$-dimensional real inner product space and let $\mathcal{B}$ be its standard orthonormal basis. Let $\text{repr} : \text{Space } d \to \mathbb{R}^d$ denote the linear isometric isomorphism that maps a vector $p$ to its coordinate representation in the Euclidean space $\mathbb{R}^d$, and let $\text{repr}^{-1}$ be its inverse mapping. For any vector $p \in \text{Space } d$ and any coordinate vector $v \in \mathbb{R}^d$, the inner product of their representations satisfies: $$\langle \text{repr}(p), v \rangle = \langle p, \text{repr}^{-1}(v) \rangle$$ where the left-hand side is the standard Euclidean inner product on $\mathbb{R}^d$ and the right-hand side is the inner product on $\text{Space } d$.

For any natural number $d$, the real vector space $\text{Space } d$ is finite-dimensional.

For any natural number $d$, the dimension of the real vector space $\text{Space } d$ is equal to $d$. That is, $\dim_{\mathbb{R}}(\text{Space } d) = d$.

For any natural number $d$, the dimension (or rank) of the real vector space $\text{Space } d$ over the field of real numbers $\mathbb{R}$ is equal to $d$. That is, $\text{rank}_{\mathbb{R}}(\text{Space } d) = d$.

For any dimension $d$, let $\phi : \text{Space } d \to \mathbb{R}^d$ be the isometric isomorphism defined by the standard orthonormal basis (the basis representation). For any point $p \in \text{Space } d$, the Fréchet derivative of $\phi$ at $p$ is equal to $\phi$ itself, considered as a continuous linear map.

For any dimension $d$, let $\phi^{-1} : \mathbb{R}^d \to \text{Space } d$ be the inverse of the coordinate representation map (the isometric isomorphism) defined by the standard orthonormal basis of $\text{Space } d$. For any vector $v \in \mathbb{R}^d$, the Fréchet derivative of $\phi^{-1}$ at the point $v$ is equal to $\phi^{-1}$ itself, considered as a continuous linear map.

For a given dimension $d$, an index $\mu \in \{0, 1, \dots, d-1\}$ (represented by `Fin d`), and a point $p$ in the space $\text{Space } d$, the coordinate function returns the $\mu$-th component of $p$. It is defined as the inner product of the point $p$ with the $\mu$-th vector of the standard orthonormal basis $e_\mu$: $$\text{coord}(\mu, p) = \langle p, e_\mu \rangle$$ This value represents the scalar projection of $p$ onto the $\mu$-th axis.

For any dimension $d$, given an index $\mu \in \{0, 1, \dots, d-1\}$ and a point $p$ in the space $\text{Space } d$, the value of the $\mu$-th coordinate function applied to $p$ is equal to the $\mu$-th component of $p$. That is, $$\text{coord}(\mu, p) = p_\mu$$

For a given dimension $d$ and an index $\mu \in \{0, 1, \dots, d-1\}$, the function $\text{coordCLM}(\mu)$ is the continuous linear map from $\text{Space } d$ to $\mathbb{R}$ that maps a vector $p$ to its $\mu$-th coordinate. It is defined as the inner product of $p$ with the $\mu$-th standard basis vector $e_\mu$: $$\text{coordCLM}(\mu)(p) = \langle p, e_\mu \rangle$$

For a given dimension $d$ and an index $i \in \{0, 1, \dots, d-1\}$, the $i$-th coordinate function on $\text{Space } d$, defined as the map $x \mapsto \text{coord}(i, x)$, is infinitely differentiable ($C^\infty$) over the real numbers $\mathbb{R}$.

For any dimension $d$, any index $\mu \in \{0, 1, \dots, d-1\}$, and any point $p \in \text{Space } d$, the value of the $\mu$-th coordinate continuous linear map $\text{coordCLM}(\mu)$ applied to $p$ is equal to the $\mu$-th coordinate of $p$: $$\text{coordCLM}(\mu)(p) = \text{coord}(\mu, p)$$ where $\text{coord}(\mu, p)$ is defined as the inner product $\langle p, e_\mu \rangle$ with the $\mu$-th standard basis vector.

The notation $\mathfrak{x}$ represents the coordinate projection function on a $d$-dimensional space $\text{Space } d$. For a given index $i$, $\mathfrak{x}_i$ maps a point in the space to its $i$-th coordinate.

In the $d$-dimensional real vector space $\text{Space } d$, for any index $i \in \{0, 1, \dots, d-1\}$, the coordinate evaluation map $p \mapsto p_i$, which maps a vector $p \in \text{Space } d$ to its $i$-th component, is continuous.

In the $d$-dimensional real vector space $\text{Space } d$, for any index $i \in \{0, 1, \dots, d-1\}$, the coordinate evaluation map $p \mapsto p_i$, which maps a vector $p \in \text{Space } d$ to its $i$-th component, is differentiable over $\mathbb{R}$.

For any dimension $d$, any order of differentiability $n$, and any index $i \in \{0, 1, \dots, d-1\}$, the $i$-th coordinate function $p \mapsto p_i$ from the $d$-dimensional real inner product space $\text{Space } d$ to $\mathbb{R}$ is $n$-times continuously differentiable ($C^n$) over $\mathbb{R}$.