Physlib.Units.WithDim.Analysis

For a physical dimension $d$ and a commutative additive monoid $M$, let $\text{WithDim}(d, M)$ be the type of values in $M$ tagged with dimension $d$. This definition provides the additive equivalence $\text{WithDim}(d, M) \simeq_{+} M$ that maps a dimension-tagged quantity to its underlying numerical value in $M$.

For a physical dimension $d$ and a type $M$ that is a normed additive commutative group, the type $\text{WithDim}(d, M)$ (representing quantities of type $M$ tagged with dimension $d$) is equipped with a normed additive commutative group structure. The norm on $\text{WithDim}(d, M)$ is induced from the norm on $M$ via the additive equivalence $\text{WithDim}(d, M) \simeq_{+} M$, such that the norm of a dimension-tagged quantity is equal to the norm of its underlying numerical value in $M$.

For a physical dimension $d$ and a type $M$ equipped with the structure of an additive commutative monoid and a module over the real numbers $\mathbb{R}$, let $\text{WithDim}(d, M)$ be the type of values in $M$ tagged with dimension $d$. This definition provides the linear equivalence $\text{WithDim}(d, M) \simeq_{\mathbb{R}} M$ that maps a dimension-tagged quantity to its underlying numerical value in $M$. This equivalence identifies the coordinates of the dimension-tagged quantity as being linear over dimensionless real scalars.

For a physical dimension $d$ and a normed space $M$ over the real numbers $\mathbb{R}$, the type $\text{WithDim}(d, M)$ (representing quantities of type $M$ tagged with dimension $d$) is equipped with a normed space structure over $\mathbb{R}$. This structure inherits the norm from $M$ such that for any $x \in \text{WithDim}(d, M)$, its norm is $\|x\| = \|x.\text{val}\|$, where $x.\text{val}$ is the underlying numerical value in $M$. This definition ensures that the norm is compatible with real scalar multiplication, satisfying the property $\|r \cdot x\| = |r| \cdot \|x\|$ for all $r \in \mathbb{R}$ and $x \in \text{WithDim}(d, M)$.

Let $d$ be a physical dimension and $M$ be a normed additive commutative group. For any dimension-tagged quantity $x$ of type $\text{WithDim}(d, M)$, the norm of $x$ is equal to the norm of its underlying numerical value $x.\text{val} \in M$, such that $\|x\| = \|x.\text{val}\|$.

Given a physical dimension $d$ and a type $M$ that is a normed space over the real numbers $\mathbb{R}$, this definition establishes a linear isometry equivalence $\text{WithDim}(d, M) \simeq_{\mathbb{R}} M$. It maps a quantity $x$ of type $M$ tagged with dimension $d$ to its underlying numerical value in $M$. This equivalence preserves the linear structure and the norm, such that for any $x \in \text{WithDim}(d, M)$, the norm $\|x\|$ is equal to the norm of its numerical value in $M$.

For a physical dimension $d$ and a type $M$ that is a normed space over the real numbers $\mathbb{R}$, let $x$ be an element of the dimension-tagged type $\text{WithDim}(d, M)$. The linear isometry equivalence $\text{toValueLinearIsometryEquiv}$ from $\text{WithDim}(d, M)$ to $M$ maps $x$ to its underlying numerical value $x.\text{val} \in M$, such that $\text{toValueLinearIsometryEquiv}(d, M)(x) = x.\text{val}$.

Let $d$ be a physical dimension and $M$ be a normed space over $\mathbb{R}$. The inverse of the linear isometry equivalence $\text{WithDim}(d, M) \simeq_{\mathbb{R}} M$ maps an element $x \in M$ to its dimension-tagged representation $\langle x \rangle$ in $\text{WithDim}(d, M)$.

Given a function $f: M \to N$ and physical dimensions $d$ and $e$ (within a base system $B$), the transport of $f$ is a function from the dimension-tagged type $\text{WithDim } d \, M$ to $\text{WithDim } e \, N$. It maps an element $x$ with dimension $d$ and numerical value $x_{\text{val}} \in M$ to an element with dimension $e$ and numerical value $f(x_{\text{val}}) \in N$.

Let $M$ and $N$ be types, and let $d$ and $e$ be physical dimensions in a base system $B$. For any function $f: M \to N$ and any dimension-tagged quantity $x \in \text{WithDim } d \, M$, the numerical value of the quantity obtained by applying the transported function $\text{transport } d \, e \, f$ to $x$ is equal to the result of applying $f$ to the numerical value of $x$. That is, $$(\text{transport } d \, e \, f(x)).\text{val} = f(x.\text{val})$$ where $x.\text{val}$ denotes the underlying numerical representation of the quantity $x$.

Let $M$ and $N$ be normed spaces over $\mathbb{R}$, and let $d$ and $e$ be physical dimensions. Given a continuous linear map $f: M \to N$, this definition constructs a corresponding continuous linear map from $\text{WithDim}(d, M)$ to $\text{WithDim}(e, N)$. It is defined by taking a quantity $x \in \text{WithDim}(d, M)$, extracting its underlying numerical value in $M$ via the canonical linear isometry $v_d: \text{WithDim}(d, M) \cong M$, applying $f$, and then tagging the resulting value in $N$ with the dimension $e$ using the inverse isometry $v_e^{-1}: N \cong \text{WithDim}(e, N)$.

Let $M$ and $N$ be normed spaces over $\mathbb{R}$, and let $d$ and $e$ be physical dimensions in a base system $B$. For any continuous linear map $f: M \to N$ and any dimension-tagged quantity $x \in \text{WithDim}(d, M)$, the underlying numerical value of the result obtained by applying the transported linear map $\text{transportLinearMap}(d, e, f)$ to $x$ is equal to the result of applying $f$ to the numerical value of $x$. That is, $$(\text{transportLinearMap}(d, e, f)(x)).\text{val} = f(x.\text{val})$$ where $x.\text{val}$ denotes the underlying numerical representation of the quantity $x$ in $M$.

Let $M$ and $N$ be normed spaces over $\mathbb{R}$, and let $d$ and $e$ be physical dimensions. Suppose a function $f: M \to N$ has a Fréchet derivative $f'$ at a point $v \in M$. Then, for any dimension-tagged quantity $x \in \text{WithDim}(d, M)$ whose underlying numerical value is $v$ (i.e., $x_{\text{val}} = v$), the transported function $\text{transport}(d, e, f): \text{WithDim}(d, M) \to \text{WithDim}(e, N)$ has a Fréchet derivative at $x$. This derivative is the transported continuous linear map $\text{transportLinearMap}(d, e, f')$.