PhyslibAlpha.AlgebraicFramework.OrderUnit.Weight.Extension

Let $E$ be an order-unit space with order unit $1$. For every element $x \in E$, there exists a real number $r$ such that $r \cdot 1 + x \ge 0$.

Let $E$ be an order-unit space and $w$ be a weight on $E$. If $w$ is finite, then for any elements $c$ and $d$ in the positive cone $\text{PosCone}(E)$, the weight of their sum is the sum of their individual weights: $$(w(c + d)).\text{toReal} = (w(c)).\text{toReal} + (w(d)).\text{toReal}$$ where $x.\text{toReal}$ denotes the conversion of the weight value from the extended non-negative real numbers ($\text{ENNReal}$) to the real numbers ($\mathbb{R}$).

Let $E$ be an order-unit space and let $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ be its positive cone. For any weight $w$ on $E$, any non-negative real scalar $k \in \mathbb{R}_{\ge 0}$, and any element $c$ in the positive cone $\text{PosCone}(E)$, the real-valued evaluation of the weight on the scaled element $k \cdot c$ is equal to $k$ times the real-valued evaluation of the weight on $c$. That is, $$\text{toReal}(w(k \cdot c)) = k \cdot \text{toReal}(w(c))$$ where $\text{toReal}$ represents the conversion of the weight's value from the extended non-negative real numbers $[0, \infty]$ to the real numbers $\mathbb{R}$.

Let $E$ be an order-unit space with order unit $1$, and let $w$ be a finite weight defined on the positive cone $\text{PosCone}(E)$. For any element $x \in E$ and any real scalar $r$ such that $r \cdot 1 + x \ge 0$, the value is defined as the real number: $$w(r \cdot 1 + x) - r \cdot w(1)$$ where $w(1)$ is the weight of the order unit. This construction calculates the value of the weight on an arbitrary element $x$ by shifting it into the positive cone and subtracting the weight associated with the shift.

Let $E$ be an order-unit space with order unit $1$, and let $w$ be a finite weight on the positive cone of $E$. For any element $x \in E$ and real numbers $r$ and $s$ such that $r \leq s$, if the shifted elements $r \cdot 1 + x$ and $s \cdot 1 + x$ both belong to the positive cone (i.e., $r \cdot 1 + x \geq 0$ and $s \cdot 1 + x \geq 0$), then the raw value of the weight at $x$ is independent of the choice between $r$ and $s$. That is, $$w(s \cdot 1 + x) - s \cdot w(1) = w(r \cdot 1 + x) - r \cdot w(1)$$ where $w(1)$ is the weight of the order unit.

Let $E$ be an order-unit space with order unit $1$, and let $w$ be a finite weight on the positive cone of $E$. For any element $x \in E$ and any real numbers $r$ and $s$ such that $r \cdot 1 + x \ge 0$ and $s \cdot 1 + x \ge 0$, the value obtained by shifting $x$ into the positive cone is independent of the choice of shift: $$w(r \cdot 1 + x) - r \cdot w(1) = w(s \cdot 1 + x) - s \cdot w(1)$$

Let $E$ be an order-unit space with order unit $1$, and let $w$ be a finite weight defined on its positive cone. The function maps an element $x \in E$ to a real value by extending the weight $w$ from the positive cone to the entire space. For any $x \in E$, the value is given by: $$x \mapsto w(r \cdot 1 + x) - r \cdot w(1)$$ where $r \in \mathbb{R}$ is any real number such that $r \cdot 1 + x \geq 0$. This value is independent of the choice of $r$.

Let $E$ be an order-unit space with order unit $1$, and let $w$ be a finite weight on its positive cone. For any element $x \in E$ and any real scalar $r$ such that $r \cdot 1 + x \ge 0$, the extension of the weight to the whole space, denoted by `toFun`, is equal to the shifted value: $$\text{toFun}(x) = w(r \cdot 1 + x) - r \cdot w(1)$$ where $w(1)$ is the weight of the order unit.

Let $E$ be an order-unit space and $w$ be a finite weight on its positive cone $\text{PosCone}(E)$. Let $W: E \to \mathbb{R}$ be the extension of $w$ to the whole space $E$ (defined by $W(x) = w(r \cdot 1 + x) - r \cdot w(1)$ for a sufficiently large $r$). For any non-negative element $x \in \text{PosCone}(E)$, the value of the extension $W(x)$ is equal to the real value of the weight $w(x)$.

Let $E$ be an order-unit space and let $w$ be a finite weight defined on its positive cone. If $W: E \to \mathbb{R}$ is the linear extension of $w$ to the whole space $E$ (defined by $W(x) = w(r \cdot 1 + x) - r \cdot w(1)$ for a sufficiently large $r$), then the value of $W$ at the zero element of $E$ is $0$, i.e., $W(0) = 0$.

Let $E$ be an order-unit space and $w$ be a finite weight defined on its positive cone. Let $W: E \to \mathbb{R}$ be the extension of $w$ to the entire space $E$, defined by $W(x) = w(r \cdot 1 + x) - r \cdot w(1)$ for any $r \in \mathbb{R}$ such that $r \cdot 1 + x \geq 0$. For any $x, y \in E$, the extension $W$ satisfies $W(x + y) = W(x) + W(y)$.

Let $E$ be an order-unit space and $w$ be a finite weight on its positive cone. Let $f: E \to \mathbb{R}$ be the extension of $w$ to the entire space $E$, defined by $f(x) = w(r \cdot 1 + x) - r \cdot w(1)$ for any $r \in \mathbb{R}$ such that $r \cdot 1 + x \ge 0$. For any $x \in E$, the extension satisfies $f(-x) = -f(x)$.

Let $E$ be an order-unit space and $w$ be a finite weight defined on its positive cone. Let $\tilde{w} : E \to \mathbb{R}$ be the unique extension of $w$ to the whole space $E$. For any $x \in E$ and any non-negative real number $t \ge 0$, the extension satisfies $\tilde{w}(t \cdot x) = t \cdot \tilde{w}(x)$.

Let $E$ be an order-unit space and $w$ be a finite weight defined on its positive cone. Let $\tilde{w} : E \to \mathbb{R}$ be the unique extension of $w$ to the whole space $E$. For any real number $t \in \mathbb{R}$ and any element $x \in E$, the extension satisfies the property of real homogeneity: $$\tilde{w}(t \cdot x) = t \tilde{w}(x)$$

Let $E$ be an order-unit space and $w$ be a finite weight on its positive cone. The $\mathbb{R}$-linear map $\tilde{w}: E \to \mathbb{R}$ is the extension of $w$ to the entire space $E$. For any $x \in E$, its value is given by $$\tilde{w}(x) = w(r \cdot 1 + x) - r \cdot w(1)$$ where $1$ is the order unit and $r \in \mathbb{R}$ is any real number such that $r \cdot 1 + x \ge 0$.

Let $E$ be an order-unit space with order unit $1$ and let $w$ be a finite weight on its positive cone. The $\mathbb{R}$-linear map extension $\tilde{w}: E \to \mathbb{R}$ evaluates at any $x \in E$ to the same value as the extension function, namely: $$\tilde{w}(x) = w(r \cdot 1 + x) - r \cdot w(1)$$ where $r \in \mathbb{R}$ is any real number such that $r \cdot 1 + x \ge 0$.

Let $E$ be an order-unit space and $w$ be a finite weight on its positive cone. The positive linear functional $\tilde{w}: E \to \mathbb{R}$ is the extension of $w$ to the entire space $E$. This map is $\mathbb{R}$-linear and satisfies the positivity condition, meaning that for any $x \in E$ such that $x \ge 0$, the value $\tilde{w}(x)$ is a non-negative real number.

Let $E$ be an order-unit space and $w$ be a finite weight on its positive cone $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$. Let $\tilde{w} : E \to \mathbb{R}$ be the positive linear functional extension of $w$. For any $x \in \text{PosCone}(E)$, the value of the extension $\tilde{w}(x)$ is equal to the value of the original weight $w(x)$ (interpreted as a real number).

Let $E$ be an order-unit space and $w$ be a finite weight on the positive cone $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$. Let $\tilde{w} : E \to \mathbb{R}$ be the unique positive linear extension of $w$ to the whole space $E$. If $f : E \to \mathbb{R}$ is any positive linear functional such that for every $x \in \text{PosCone}(E)$, the value $f(x)$ equals the real value of $w(x)$, then $f = \tilde{w}$.