PhyslibAlpha.ProbabilisticTheory.Classical.PureState

Given a positive linear map $\phi : E \to \mathbb{R}$ and a proof that its value at the identity element is strictly positive ($\phi(1) > 0$), this definition constructs a unital positive linear map (a state) by scaling $\phi$ by the scalar $(\phi(1))^{-1}$. The resulting state $\psi \in \mathcal{S}[\mathbb{R}, E]$ maps each element $f \in E$ to $\frac{\phi(f)}{\phi(1)}$, ensuring that $\psi(1) = 1$.

Let $E$ be an order-unit space. For any positive linear map $\phi : E \to \mathbb{R}$ such that $\phi(1) > 0$, the value of the normalized map (the state associated with $\phi$) at an element $f \in E$ is equal to $(\phi(1))^{-1} \phi(f)$.

Let $E$ be a real vector space and let $\omega \in \mathcal{S}[\mathbb{R}, E]$ be a state, which is defined as a unital positive linear map from $E$ to $\mathbb{R}$. For any element $f \in E$, the value of the underlying positive linear map of $\omega$ applied to $f$ is equal to $\omega(f)$.

Let $E$ be an order-unit space. Let $\omega$ be a pure state on $E$ and $\phi$ be a positive linear functional such that $\phi \le \omega$. If $0 < \phi(1) < 1$, then for any element $f \in E$, $\phi(f) = \phi(1) \omega(f)$. Here, $1$ denotes the order unit of $E$.

Let $E$ be an order-unit space. Suppose $\omega \in \mathcal{S}(E)$ is a pure state and $\varphi: E \to \mathbb{R}$ is a positive linear map. If $\varphi \leq \omega$ (meaning $\varphi(x) \leq \omega(x)$ for all $x \geq 0$ in $E$), then for every $f \in E$, the identity $$\varphi(f) = \varphi(\mathbb{1}) \omega(f)$$ holds, where $\mathbb{1}$ denotes the order unit of $E$. In other words, any positive linear map dominated by a pure state must be a scalar multiple of that pure state.

Given a state $\omega$ (a unital positive linear map) and a non-negative scalar $c \in \mathbb{R}_{\ge 0}$, the weighted map is the positive linear map $c\omega$ defined by $(c\omega)(f) = c \cdot \omega(f)$ for any observable $f \in E$.

Let $E$ be an order-unit space. For any state $\omega \in \mathcal{S}(E)$, any non-negative real scalar $c \in \mathbb{R}_{\ge 0}$, and any observable $f \in E$, the value of the weighted map $c\omega$ applied to $f$ is given by the formula $$(c\omega)(f) = c \cdot \omega(f).$$

Let $E$ be an order-unit space and $\omega$ be a pure state on $E$. Let $\gamma: E \to \mathbb{R}$ be a positive linear map and $c \ge 0$ be a non-negative scalar. If $\gamma \le c\omega$ (meaning $\gamma(f) \le c \cdot \omega(f)$ for all $f \ge 0$ in $E$), then for any observable $f \in E$, it holds that $\gamma(f) = \gamma(1) \cdot \omega(f)$.

Let $E$ be an Archimedean order-unit space and let $\mathcal{S}(E)$ denote its state space (the set of normalized positive continuous linear functionals). For any two states $x, y \in \mathcal{S}(E)$ and any real numbers $p, q \in \mathbb{R}$, if $x = y$ implies $p = q$, then there exists an observable $a \in E$ such that $x(a) = p$ and $y(a) = q$.

Given an Archimedean order-unit space $E$, `PureState E` is the type representing the set of pure states. It is defined as the subtype of the state space $\mathcal{S}(E)$ consisting of those states $\omega$ that satisfy the property `IsPure`, meaning $\omega$ is an extreme point of the convex set $\mathcal{S}(E)$. This space is equipped with the weak-star topology inherited from the weak dual space $E^*$.

Given an Archimedean order-unit space $E$, this $\mathbb{R}$-linear map associates each observable $a \in E$ with a continuous real-valued function on the space of pure states $\text{PureState } E$. For any pure state $\omega \in \text{PureState } E$, the value of this function is the evaluation of the state on the observable, denoted $\omega(a)$. This representation realizes an observable as a continuous function of its values on pure states.

Let $E$ be an Archimedean order-unit space. For any observable $f \in E$ and any pure state $\omega \in \text{PureState } E$, the value of the continuous function $\text{evalPure}(f)$ evaluated at $\omega$ is equal to the value of the state $\omega$ applied to $f$, denoted $\omega(f)$.

Let $E$ be an Archimedean order-unit space with order unit $\mathbf{1}$. The evaluation map $\text{evalPure} : E \to C(\text{PureState } E, \mathbb{R})$, which associates each observable $a \in E$ with the continuous function $\omega \mapsto \omega(a)$ on the space of pure states, satisfies $\text{evalPure}(\mathbf{1}) = 1$, where $1$ on the right-hand side represents the constant function that takes the value $1$ for all pure states.

Let $E$ be an Archimedean order-unit space. For any element $f \in E$, if $\omega(f) \ge 0$ for every pure state $\omega \in \text{PureState } E$, then $f \ge 0$.

Let $E$ be an Archimedean order-unit space. For any observables $f, g \in E$, the inequality $f \le g$ holds if and only if $\omega(f) \le \omega(g)$ for every pure state $\omega \in \text{PureState } E$. This is equivalent to saying that $f \le g$ if and only if $\text{evalPure } f \le \text{evalPure } g$ in the space of continuous functions $C(\text{PureState } E, \mathbb{R})$, where $\text{evalPure } f(\omega) = \omega(f)$.