PhyslibAlpha.ProbabilisticTheory.Classical.SimplexStateSpace

Let $E$ be an Archimedean order-unit space and $\omega \in \mathcal{S}(E)$ be a state, which is a unital positive linear map from $E$ to $\mathbb{R}$. The state $\omega$ has a pure decomposition if there exists a regular probability measure $\mu$ on the set of pure states of $E$ such that $\omega$ is represented by $\mu$. Specifically, for every element $f \in E$, the value of the functional is given by the integral: $$\omega(f) = \int_{\text{PureState } E} \phi(f) \, d\mu(\phi)$$ where the integration is performed over the set of pure states $\phi$.

Let $E$ be an Archimedean order-unit space and let $\omega \in \mathcal{S}(\mathbb{R}, E)$ be a state (a unital positive linear map from $E$ to $\mathbb{R}$). The state $\omega$ has a unique pure decomposition if there exists exactly one regular probability measure $\mu$ supported on the set of pure states of $E$ that represents $\omega$. In this context, a measure $\mu$ represents $\omega$ if for every observable $f \in E$, the value $\omega(f)$ is given by the integral of the evaluation maps $\phi \mapsto \phi(f)$ over the pure states $\phi$ with respect to $\mu$.

For an Archimedean order-unit space $E$, the property `IsSimplexStateSpace` states that the state space $\mathcal{S}(E)$ is a simplex. This means that every state $\omega \in \mathcal{S}(E)$ can be uniquely represented as a mixture of pure states, specifically by a unique regular probability measure on the set of pure states. In finite dimensions, this corresponds to the state space being the convex hull of affinely independent pure states, where every state has unique barycentric coordinates.

For an Archimedean order-unit space $E$, the property `IsBauerSimplexStateSpace` states that the state space $\mathcal{S}(E)$ is a Bauer simplex. This means that: 1. $\mathcal{S}(E)$ is a simplex, where every state $\omega \in \mathcal{S}(E)$ is uniquely represented by a regular probability measure on the set of pure states. 2. The set of pure states $\{\omega \in \mathcal{S}(E) \mid \omega \text{ is pure}\}$ is a closed set in the weak-* topology.

Let $E$ be an Archimedean order-unit space. For any finite measure $\mu$ on the space of pure states $\text{PureState}(E)$ and any element $f \in E$, the function that maps each pure state $\omega$ to its value $\omega(f)$ is integrable with respect to $\mu$.

Given a finite measure $\mu$ on the set of pure states $\text{PureState}(E)$ of an Archimedean order-unit space $E$, this function defines a positive linear functional $L: E \to \mathbb{R}$ by integrating an observable $f \in E$ against the measure $\mu$: $$L(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$$ where each $\omega \in \text{PureState}(E)$ is treated as a state (a normalized positive linear functional) acting on the element $f$.

Let $E$ be an Archimedean order-unit space. For any finite measure $\mu$ on the set of pure states $\text{PureState}(E)$ and any observable $f \in E$, the value of the positive linear functional $L_\mu$ (constructed from $\mu$ via `toPositive`) applied to $f$ is equal to the integral of the evaluations $\omega(f)$ over the pure states with respect to the measure $\mu$: $$L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$$ where each pure state $\omega$ is treated as a normalized positive linear functional acting on $f$.

Let $E$ be an Archimedean order-unit space and let $\text{PureState}(E)$ denote its set of pure states. For any finite measures $\mu$ and $\nu$ on $\text{PureState}(E)$, the mapping $\text{toPositive}$ that associates a measure with a positive linear functional is additive: $$\text{toPositive}(\mu + \nu) = \text{toPositive}(\mu) + \text{toPositive}(\nu)$$ Here, $\text{toPositive}(\mu)$ is the positive linear functional $L: E \to \mathbb{R}$ defined by the integral $L(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$ for $f \in E$.

Let $E$ be an Archimedean order-unit space. Suppose $\mu$ and $\nu$ are finite measures on the set of pure states $\text{PureState}(E)$. If $\mu \le \nu$ (meaning $\mu(A) \le \nu(A)$ for all measurable sets $A$), then the corresponding positive linear functionals $L_\mu$ and $L_\nu$ satisfy $L_\mu \le L_\nu$. The positive linear functional $L_\mu: E \to \mathbb{R}$ associated with a measure $\mu$ is defined by: $$L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$$ where $\omega(f)$ denotes the evaluation of the state $\omega$ at the observable $f \in E$. The inequality $L_\mu \le L_\nu$ means that $L_\mu(f) \le L_\nu(f)$ for all $f \in E$ such that $f \ge 0$.

Let $E$ be an Archimedean order-unit space with order unit $\mathbf{1}$. For any finite measure $\mu$ on the set of pure states $\text{PureState}(E)$, let $L_\mu: E \to \mathbb{R}$ be the positive linear functional defined by $L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$. Then the value of the functional evaluated at the order unit $\mathbf{1}$ is equal to the total mass of the measure $\mu$ on the set of pure states: $$L_\mu(\mathbf{1}) = \mu(\text{PureState}(E))$$

Let $E$ be an Archimedean order-unit space. Let $\mu$ and $\nu$ be finite measures on the set of pure states $\text{PureState}(E)$. Let $L_\mu$ and $L_\nu$ be the positive linear functionals associated with these measures, defined by $L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$ and $L_\nu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\nu(\omega)$ for any $f \in E$. If these associated functionals are equal ($L_\mu = L_\nu$), then the total mass of the measures is equal: $\mu(\text{PureState}(E)) = \nu(\text{PureState}(E))$.

Let $E$ be an Archimedean order-unit space and $\text{PureState}(E)$ be the set of its pure states. Given two finite measures $\mu$ and $\nu$ on $\text{PureState}(E)$, let $L_\mu$ and $L_\nu$ be the positive linear functionals defined by integration: $$L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$$ If $L_\mu = L_\nu$, then for any scalar $c \in [0, \infty]$ such that the scaled measures $c\mu$ and $c\nu$ are finite, it holds that $L_{c\mu} = L_{c\nu}$.

Let $E$ be an Archimedean order-unit space whose state space is a simplex. For every positive linear functional $\alpha : E \to \mathbb{R}$, there exists a finite regular measure $\mu$ on the set of pure states $\text{PureState}(E)$ such that $\alpha$ is the functional obtained by integrating over the pure states. That is, for all $f \in E$: $$\alpha(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega)$$ where $\omega \in \text{PureState}(E)$ are the pure states of the system.

Let $E$ be an Archimedean order-unit space whose state space is a simplex. Let $\mu$ and $\theta$ be regular finite measures on the set of pure states $\text{PureState}(E)$. Define the positive linear functionals $L_\mu, L_\theta: E \to \mathbb{R}$ by integrating observables against these measures: $$L_\mu(f) = \int_{\text{PureState}(E)} \omega(f) \, d\mu(\omega) \quad \text{and} \quad L_\theta(f) = \int_{\text{PureState}(E)} \omega(f) \, d\theta(\omega)$$ If $L_\mu \le L_\theta$ (meaning $L_\mu(f) \le L_\theta(f)$ for all $f \in E$ such that $f \ge 0$), then $\mu \le \theta$ as measures.