PhyslibAlpha.AlgebraicFramework.OrderUnit.State.WeightBridge

For a weight $w$ on a space $E$ that satisfies the condition of being a state (i.e., it is normalized and positive), this definition provides the underlying function from $E$ to $\mathbb{R}$ corresponding to its finite-weight extension.

Given a weight $w$ on a real vector space $E$ that satisfies the condition of being a state ($w.\text{IsState}$), this definition provides its extension as a linear map from $E$ to $\mathbb{R}$.

Given a weight $w$ on a real vector space $E$ that satisfies the condition of being a state (denoted by $w.\text{IsState}$, meaning it is finite and normalized), this function constructs the corresponding state as a unital positive linear map from $E$ to $\mathbb{R}$. The resulting map $\phi \in \mathcal{S}[\mathbb{R}, E]$ is obtained by extending $w$ to a linear map such that $\phi(1) = 1$ and $\phi(x) \geq 0$ for all $x \geq 0$.

Let $w$ be a weight on a real vector space $E$. If $w$ satisfies the condition of being a state (i.e., it is finite and normalized), let $\phi \in \mathcal{S}[\mathbb{R}, E]$ be the state (unital positive linear map) constructed from $w$. Then for any $x \in E$, the value $\phi(x)$ is equal to the value of the underlying function $f: E \to \mathbb{R}$ associated with the state weight $w$ at $x$.

Given a state $s \in \mathcal{S}[\mathbb{R}, E]$ on an ordered real vector space $E$, the weight induced by $s$ is the map $\omega: \text{PosCone}(E) \to [0, \infty]$ defined by $\omega(x) = s(x)$ for all $x \in \text{PosCone}(E)$. Here, $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$ is the positive cone of $E$, and the real value $s(x)$ is embedded into the extended non-negative real numbers $[0, \infty]$. Since $s$ is a positive linear map, $s(x) \ge 0$ for all $x$ in the positive cone, ensuring no information is lost during the conversion to $[0, \infty]$.

For any state $s \in \mathcal{S}[\mathbb{R}, E]$ and any element $x$ in the positive cone $\text{PosCone}(E) = \{x \in E \mid 0 \le x\}$, the value of the weight induced by $s$ at $x$ is equal to the result of applying $s$ to $x$ (viewed as an element of the vector space $E$) and converting the resulting real number to an extended non-negative real number $[0, \infty]$. That is, $(s.\text{toWeight})(x) = \text{ofReal}(s(x))$.

Let $E$ be an ordered real vector space. For any state $s \in \mathcal{S}[\mathbb{R}, E]$ and any element $x$ in the positive cone $\text{PosCone}(E)$, the value of the weight induced by $s$ at $x$, when converted back to a real number, is equal to the value of the state $s$ applied to $x$. That is, $(s.\text{toWeight}(x)).\text{toReal} = s(x)$.

For any state $s \in \mathcal{S}[\mathbb{R}, E]$ on an ordered real vector space $E$, the weight induced by $s$ (denoted $s.\text{toWeight}$) is itself a state weight. This means the weight is finite (its values in $[0, \infty]$ never reach $\infty$) and normalized (it maps the order unit of $E$ to $1$).

Let $E$ be an ordered real vector space. There is an equivalence (a bijective correspondence) between the set of state weights on $E$ and the set of states $\mathcal{S}[\mathbb{R}, E]$. A state weight is a weight $w: \text{PosCone}(E) \to [0, \infty]$ that is finite (takes values in $\mathbb{R}_{\ge 0}$) and normalized (maps the order unit to $1$). A state $s \in \mathcal{S}[\mathbb{R}, E]$ is a unital positive linear functional from $E$ to $\mathbb{R}$. This equivalence maps a state weight to its linear extension on $E$ and maps a state to its restriction to the positive cone $\text{PosCone}(E)$.