PhyslibAlpha.AlgebraicFramework.OrderUnit.Norm

Given an element $x$ in an ordered space $E$ with an Archimedean order unit $1$, the set of order-unit bounds is the set of all non-negative real numbers $r \in \mathbb{R}$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Given an element $x$ in an ordered space $E$ with an Archimedean order unit $1$, the order-unit norm of $x$ is defined as the infimum of the set of all non-negative real numbers $r \in \mathbb{R}$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$, the set of order-unit bounds $\{r \in \mathbb{R} \mid r \ge 0 \text{ and } -r \cdot 1 \le x \le r \cdot 1\}$ is non-empty.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$, the set of order-unit bounds $\{r \in \mathbb{R} \mid -r \cdot 1 \le x \le r \cdot 1\}$ is bounded below in $\mathbb{R}$. Specifically, this set is bounded below by $0$.

Let $E$ be an ordered space with an Archimedean order unit. For any element $x \in E$, the order-unit norm of $x$, denoted as $\|x\|$, is non-negative, i.e., $0 \le \|x\|$. The order-unit norm is defined as the infimum of the set of non-negative real numbers $r$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$ and any real number $r \in \mathbb{R}$, if $r$ is an order-unit bound of $x$ (that is, $r$ satisfies $-r \cdot 1 \le x \le r \cdot 1$), then the order-unit norm of $x$ is less than or equal to $r$ ($\|x\| \le r$).

Let $E$ be an ordered space with an Archimedean order unit. The order-unit norm of the zero element $0 \in E$ is $0$, i.e., $\text{orderUnitNorm}(0) = 0$.

For any element $x$ in an ordered space $E$ with an Archimedean order unit $1$, the set of order-unit bounds of $-x$ is equal to the set of order-unit bounds of $x$. Here, the set of order-unit bounds of $x$ is the set of non-negative real numbers $r \in \mathbb{R}$ such that $-r \cdot 1 \le x \le r \cdot 1$.

For any element $x$ in an ordered space $E$ with an Archimedean order unit, the order-unit norm of the negation of $x$ is equal to the order-unit norm of $x$, that is, $\text{orderUnitNorm}(-x) = \text{orderUnitNorm}(x)$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any elements $x, y \in E$ and real numbers $r, s \in \mathbb{R}$, if $r$ is an order-unit bound of $x$ (that is, $-r \cdot 1 \le x \le r \cdot 1$) and $s$ is an order-unit bound of $y$ (that is, $-s \cdot 1 \le y \le s \cdot 1$), then their sum $r + s$ is an order-unit bound of $x + y$ (that is, $-(r + s) \cdot 1 \le x + y \le (r + s) \cdot 1$).

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$ and any real number $\varepsilon > 0$, there exists an order-unit bound $r$ of $x$ (that is, a real number $r$ satisfying $-r \cdot 1 \le x \le r \cdot 1$) such that $r$ is strictly less than the sum of the order-unit norm of $x$ and $\varepsilon$: $$r < \|x\| + \varepsilon$$ where $\|x\|$ denotes the order-unit norm of $x$, defined as the infimum of all such bounds $r$.

Let $E$ be an ordered space with an Archimedean order unit. For any elements $x, y \in E$, the order-unit norm $\|\cdot\|$ satisfies the triangle inequality: $$\|x + y\| \leq \|x\| + \|y\|$$ where the order-unit norm $\|x\|$ is defined as the infimum of all $r \in \mathbb{R}$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. If the order-unit norm of an element $x \in E$ is zero (i.e., $\text{orderUnitNorm}(x) = 0$), then for any real number $\varepsilon > 0$, the element $x$ is bounded above by the $\varepsilon$-multiple of the unit, such that $x \le \varepsilon \cdot 1$.

In an ordered space $E$ with an Archimedean order unit $1$, the order-unit norm of an element $x \in E$, denoted by $\text{orderUnitNorm}(x)$, is equal to $0$ if and only if $x = 0$.

In an ordered space $E$ with an Archimedean order unit $1$, the order-unit norm $\|\cdot\|$ is the additive group norm defined by $\|x\| = \inf \{r \in \mathbb{R}_{\ge 0} \mid -r \cdot 1 \le x \le r \cdot 1\}$. This structure packages the function $x \mapsto \text{orderUnitNorm}(x)$ with the necessary proofs that it satisfies the norm axioms: $\|0\| = 0$, the triangle inequality $\|x + y\| \le \|x\| + \|y\|$, the symmetry property $\|-x\| = \|x\|$, and the positive definiteness property $\|x\| = 0 \iff x = 0$.

In an ordered additive commutative group $E$ equipped with an Archimedean order unit $1$, this definition establishes the structure of a normed additive commutative group (`NormedAddCommGroup`) on $E$. The norm used is the order-unit norm $\|x\|$, which is defined as the infimum of all $r \in \mathbb{R}_{\ge 0}$ such that $-r \cdot 1 \le x \le r \cdot 1$. This structure equips $E$ with a metric space topology where the distance between two elements $x$ and $y$ is given by $\|x - y\|$.

In an ordered space $E$ with an Archimedean order unit $1$, for any element $x \in E$, the inequality $x \le \|x\| \cdot 1$ holds, where $\|x\|$ denotes the order-unit norm of $x$. This norm $\|x\|$ is defined as the infimum of the set of all non-negative real numbers $r$ such that $-r \cdot 1 \le x \le r \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$, the inequality $-\|x\| \cdot 1 \le x$ holds, where $\|x\|$ is the order-unit norm of $x$, defined as the infimum of the set of all non-negative real numbers $r$ such that $-r \cdot 1 \le x \le r \cdot 1$.

In an ordered space $E$ with an Archimedean order unit $1$, for any element $x \in E$, the order-unit norm of $x$, denoted as $\|x\|$, is itself an order-unit bound of $x$. That is, the infimum defining the norm is attained, satisfying the inequality $-\|x\| \cdot 1 \le x \le \|x\| \cdot 1$.

Let $E$ be an ordered space with an Archimedean order unit $1$. For any element $x \in E$ and any real number $r \in \mathbb{R}$, $r$ is an order-unit bound of $x$ (that is, $-r \cdot 1 \le x \le r \cdot 1$) if and only if $r$ is greater than or equal to the order-unit norm of $x$, denoted as $\text{orderUnitNorm } x$.

Given an ordered additive commutative group $E$ with an Archimedean order unit $1$, this definition establishes a normed space structure over the real numbers $\mathbb{R}$ on $E$. The norm is the order-unit norm $\|x\|$, defined for any $x \in E$ as the infimum of the set of all $r \in \mathbb{R}_{\ge 0}$ such that $-r \cdot 1 \le x \le r \cdot 1$. This structure is built upon the normed additive commutative group structure previously induced by the same order-unit norm.

Let $E$ be an ordered additive commutative group with an Archimedean order unit. The set of non-negative elements $\{x \in E \mid 0 \le x\}$ (the positive cone) is closed in the topology induced by the order-unit norm $\|x\| = \inf \{r \in \mathbb{R}_{\ge 0} \mid -r \cdot 1 \le x \le r \cdot 1\}$.

For any real number $x \in \mathbb{R}$, the order-unit norm of $x$ (defined with respect to the classical order unit $1$) is equal to its absolute value $|x|$.

Let $E$ be a type (typically an ordered vector space with an Archimedean order unit). `WithOrderUnitNorm E` is a type synonym for $E$ that is canonically equipped with the order-unit norm. For an element $x \in E$, this norm is defined as $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$, where $\mathbf{1}$ is the order unit. This construction allows $E$ to carry the order-unit norm structure even if the original type $E$ is already equipped with a different norm for other purposes.

The type synonym `WithOrderUnitNorm E`, representing the type $E$ equipped with the order-unit norm, inherits the additive commutative group structure from the underlying type $E$. This means the operations of addition, negation, and the zero element on `WithOrderUnitNorm E` are identical to those defined on $E$.

The type synonym `WithOrderUnitNorm E`, representing the type $E$ equipped with the order-unit norm, inherits the module structure over the real numbers $\mathbb{R}$ from the underlying type $E$. This defines the scalar multiplication of elements in `WithOrderUnitNorm E` by real numbers.

The type synonym `WithOrderUnitNorm E` inherits the partial order structure $\le$ from the underlying type $E$.

The type synonym `WithOrderUnitNorm E`, which represents the space $E$ equipped with the order-unit norm, inherits the structure of an ordered additive monoid from $E$. This means that the addition operation and the partial order $\le$ are compatible: for any elements $a, b, c \in \text{WithOrderUnitNorm } E$, if $a \le b$, then $a + c \le b + c$.

In the space $E$ equipped with the order-unit norm, scalar multiplication by non-negative real numbers is monotone. Specifically, for any real number $r \ge 0$ and any elements $x, y \in E$, if $x \le y$, then $r \cdot x \le r \cdot y$.

The type `WithOrderUnitNorm E` is equipped with a unit element $1$, which represents the order unit $\mathbf{1}$ used in the definition of the order-unit norm and for comparing elements within the ordered space.

In the space $E$ equipped with the order-unit norm, the unit element $1$ is an order unit. This means that for every element $x \in E$, there exists a real number $r$ such that $-r \cdot 1 \le x \le r \cdot 1$, where $\le$ is the partial order inherited from $E$.

In the type synonym `WithOrderUnitNorm E`, which represents the space $E$ equipped with the order-unit norm, the unit element $1$ is an Archimedean order unit. This implies that $1$ is an order unit for the space and that the order structure satisfies the Archimedean property, allowing the order-unit norm to be well-defined as a genuine norm.

Let $E$ be an ordered additive commutative group with an Archimedean order unit $\mathbf{1}$. The type `WithOrderUnitNorm E` (a type synonym for $E$) is equipped with the structure of a normed additive commutative group. The norm $\| \cdot \|$ on this group is the order-unit norm, defined as $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$.

Let $E$ be an ordered vector space with an Archimedean order unit $\mathbf{1}$. The type synonym `WithOrderUnitNorm E` is canonically equipped with the structure of a normed space over the real numbers $\mathbb{R}$. The norm $\|\cdot\|$ associated with this structure is the order-unit norm, defined for any element $x \in E$ as $$\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$$ This definition ensures that the scalar multiplication and addition in $E$ are compatible with the topology induced by this norm.

Let $E$ be a real vector space (typically an ordered vector space with an Archimedean order unit). This is the $\mathbb{R}$-linear equivalence between $E$ and its type synonym `WithOrderUnitNorm E`, which is the space $E$ equipped with the order-unit norm $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$. The map is the identity on the underlying elements.

Let $E$ be a real vector space and let $\text{WithOrderUnitNorm } E$ be the type synonym for $E$ equipped with the order-unit norm. The canonical $\mathbb{R}$-linear equivalence $\phi : E \simeq_{\mathbb{R}} \text{WithOrderUnitNorm } E$ acts as the identity map on the underlying elements, such that for any $x \in E$, $\phi(x) = x$.

Let $E$ be an ordered vector space with an Archimedean order unit $\mathbf{1}$. For any element $x$ in the type synonym $\text{WithOrderUnitNorm } E$ (representing $E$ equipped with the order-unit norm), the norm $\|x\|$ is equal to the order-unit norm of the corresponding element in $E$, which is defined as $\inf \{ r \in \mathbb{R} \mid -r \cdot \mathbf{1} \le x \le r \cdot \mathbf{1} \}$.

The linear isometry equivalence between the real numbers $\mathbb{R}$ equipped with the order-unit norm and the standard real numbers $\mathbb{R}$ with the absolute value norm. For an element $x \in \mathbb{R}$, the order-unit norm induced by the unit $1$ is defined as $\|x\| = \inf \{ r \in \mathbb{R} \mid -r \le x \le r \}$, which is equal to the standard absolute value $|x|$. This equivalence acts as the canonical identification between the order-unit space structure of $\mathbb{R}$ and its standard topological and normed structure.

Let $x$ be a real number viewed as an element of the type synonym $\text{WithOrderUnitNorm } \mathbb{R}$. The application of the linear isometry equivalence `realLinearIsometryEquiv` to $x$ results in the real number $x$.

The set of real numbers $\mathbb{R}$, equipped with the order-unit norm $\|\cdot\|$ induced by the order unit $1$ (where $\|x\| = |x|$), is a complete space.

Let $E$ and $F$ be ordered vector spaces equipped with Archimedean order units. For any unital positive linear map $\phi : E \to F$ and any element $x \in E$, the order-unit norm of the image $\phi(x)$ is bounded by the order-unit norm of $x$: $$\|\phi(x)\| \leq \|x\|$$ where the order-unit norm $\|\cdot\|$ is defined as $\|y\| = \inf \{r \in \mathbb{R}_{\ge 0} \mid -r \cdot 1 \le y \le r \cdot 1\}$.