PhyslibAlpha.ProbabilisticTheory.Classical.FiniteSystem

For a set of outcomes $\iota$, the finite classical system is defined as the space of real-valued functions $f: \iota \to \mathbb{R}$. These functions represent the observables of the system and are typically considered with a pointwise ordering.

For a finite set of outcomes $\iota$, the space of observables $\text{FiniteClassicalSystem}(\iota)$, consisting of real-valued functions $f: \iota \to \mathbb{R}$ with pointwise ordering, is an order-unit space. The constant function $1$ (defined by $1(i) = 1$ for all $i \in \iota$) serves as the order unit, satisfying $1 \ge 0$ and the property that for any observable $A$, there exists a natural number $n$ such that $A \le n \cdot 1$.

For a set of outcomes $\iota$, the space of observables $\text{FiniteClassicalSystem}(\iota)$, consisting of real-valued functions $f: \iota \to \mathbb{R}$ with the constant function $1$ as its order unit, is an Archimedean order-unit space. This means that for any observable $A$, if $A \le \epsilon \cdot 1$ holds pointwise for every $\epsilon > 0$ in $\mathbb{R}$, then $A \le 0$.

For a finite set of outcomes $\iota$ and the corresponding space of observables $\text{FiniteClassicalSystem } \iota$ (consisting of functions $A: \iota \to \mathbb{R}$), the function $\text{eval}(i)$ maps an outcome $i \in \iota$ to a state in the state space $\mathcal{S}[\mathbb{R}, \text{FiniteClassicalSystem } \iota]$. This state acts on an observable $A$ by evaluating it at $i$, such that $\text{eval}(i)(A) = A(i)$. It represents the deterministic state where the outcome $i$ is obtained with certainty.

Let $\iota$ be a finite set of outcomes. Let $A \in \text{FiniteClassicalSystem}(\iota)$ be an observable, represented as a real-valued function $A: \iota \to \mathbb{R}$. For any outcome $i \in \iota$, let $\text{eval}(i)$ be the deterministic state corresponding to $i$. Then, the evaluation of the state $\text{eval}(i)$ on the observable $A$ is given by: $$\text{eval}(i)(A) = A(i)$$

Let $\iota$ be a finite set of outcomes. Let $V$ be the finite classical system with outcomes $\iota$, defined as the space of real-valued functions $A: \iota \to \mathbb{R}$. For any linear functional $f: V \to \mathbb{R}$ and any observable $A \in V$, the value of $f$ applied to $A$ is given by the sum: $$f(A) = \sum_{i \in \iota} A(i) f(\delta_i)$$ where $\delta_i$ is the indicator function (defined by `Pi.single i 1`) which takes the value $1$ at $i$ and $0$ otherwise. This demonstrates that a linear functional on a finite classical system is uniquely determined by its values on the individual outcomes.

The linear isomorphism `dualEquiv` identifies the dual space of a finite classical system (the space of real linear functionals $f: \text{FiniteClassicalSystem}(\iota) \to \mathbb{R}$) with the space of functions $\iota \to \mathbb{R}$. For a linear functional $f$, the corresponding vector in $\iota \to \mathbb{R}$ is given by its values on the elementary outcomes, $i \mapsto f(\delta_i)$, where $\delta_i$ is the indicator function that is $1$ at $i$ and $0$ elsewhere. Its inverse maps a vector $p \in \iota \to \mathbb{R}$ to the linear functional defined by $f(A) = \sum_{i \in \iota} p_i A_i$ for any observable $A \in \text{FiniteClassicalSystem}(\iota)$.

Let $\iota$ be a set of outcomes and $V$ be the finite classical system, defined as the space of real-valued functions $A: \iota \to \mathbb{R}$. Let $\Phi: V^* \cong \mathbb{R}^\iota$ be the linear isomorphism `dualEquiv` that identifies the dual space of $V$ with the space of functions on $\iota$. For any linear functional $f \in V^*$ and any outcome $i \in \iota$, the $i$-th component of $\Phi(f)$ is given by the value of $f$ applied to the indicator function $\delta_i$: $$\Phi(f)_i = f(\delta_i)$$ where $\delta_i$ (represented by `Pi.single i 1`) is the function that is $1$ at $i$ and $0$ elsewhere.

In a finite classical system with outcomes $\iota$, the observables are real-valued functions $A: \iota \to \mathbb{R}$. The inverse of the linear isomorphism $\text{dualEquiv}$ maps a vector $p: \iota \to \mathbb{R}$ to a linear functional on the space of observables. For any such vector $p$ and any observable $A$, the evaluation of this functional is given by the sum $$(\text{dualEquiv}^{-1} p)(A) = \sum_{i \in \iota} p_i A_i.$$

Given a probability vector $p$ in the standard simplex $\Delta^\iota$ (defined as the set of functions $p: \iota \to \mathbb{R}$ such that $p_i \ge 0$ for all $i$ and $\sum_{i \in \iota} p_i = 1$), this definition constructs the corresponding state $\omega$ on the finite classical system $\text{FiniteClassicalSystem}(\iota)$. This state is a unital positive linear map that maps an observable $A: \iota \to \mathbb{R}$ to the value $\omega(A) = \sum_{i \in \iota} p_i A_i$, representing the state where each outcome $i \in \iota$ is assigned the probability $p_i$.

In a finite classical system with a set of outcomes $\iota$, let $p: \iota \to \mathbb{R}$ be a probability vector in the standard simplex $\Delta^\iota$ (i.e., $p_i \ge 0$ and $\sum p_i = 1$). For any observable $A$, represented as a real-valued function $A: \iota \to \mathbb{R}$, the state $\text{ofProbs}(p)$ evaluated at $A$ is given by the weighted sum: $$\text{ofProbs}(p)(A) = \sum_{i \in \iota} p_i A_i$$

For a finite set of outcomes $\iota$, let $V = \text{FiniteClassicalSystem}(\iota)$ be the order-unit space of observables (real-valued functions on $\iota$). Let $\mathcal{S}(V) \subseteq V^*$ be the algebraic state space, consisting of the unital positive linear functionals on $V$. Let $\Phi : V^* \to \mathbb{R}^\iota$ be the linear isomorphism (`dualEquiv`) that maps a functional $\omega$ to the vector $p \in \mathbb{R}^\iota$ defined by $p_i = \omega(\delta_i)$, where $\delta_i$ is the indicator function of the outcome $i$. Then the image of the algebraic state space under this isomorphism is the standard simplex of probability vectors on $\iota$: $$\Phi(\mathcal{S}(V)) = \{ p \in \mathbb{R}^\iota \mid \sum_{i \in \iota} p_i = 1, \text{ and } p_i \ge 0 \text{ for all } i \in \iota \}.$$

For a finite set of outcomes $\iota$, let $\text{FiniteClassicalSystem}(\iota)$ be the order-unit space of observables, consisting of real-valued functions $f: \iota \to \mathbb{R}$. This equivalence identifies the state space $\mathcal{S}$ of the system (the set of unital positive linear functionals on the observables) with the standard simplex $\Delta^\iota$ of probability vectors: $$\Delta^\iota = \left\{ p \in \mathbb{R}^\iota \mid p_i \ge 0 \text{ for all } i \in \iota, \text{ and } \sum_{i \in \iota} p_i = 1 \right\}.$$ Specifically, a state $\omega$ is mapped to the probability vector $p$ where $p_i = \omega(\delta_i)$, with $\delta_i$ being the indicator function for outcome $i$. Conversely, a probability vector $p$ corresponds to the state $\omega$ defined by the weighted sum $\omega(A) = \sum_{i \in \iota} p_i A_i$ for any observable $A$.

For a finite classical system with a set of outcomes $\iota$, let $\omega$ be a state (a unital positive linear functional on the space of real-valued observables). The equivalence $\text{stateEquiv}$ maps the state $\omega$ to a probability vector in $\mathbb{R}^\iota$. For any outcome $i \in \iota$, the $i$-th component of this probability vector is given by the value of the state applied to the indicator function $\delta_i$ (the function that is $1$ at $i$ and $0$ elsewhere): $$(\text{stateEquiv } \omega)_i = \omega(\delta_i).$$

For a finite classical system with a set of outcomes $\iota$, let $\text{eval}(i)$ be the deterministic state (the linear functional that maps an observable $A: \iota \to \mathbb{R}$ to its value $A(i)$). Under the linear isomorphism $\text{dualEquiv}$, which identifies the dual space of the observables with the space of functions $\iota \to \mathbb{R}$, the image of $\text{eval}(i)$ is the indicator function $\delta_i$ (the function that is $1$ at $i$ and $0$ elsewhere).

In a finite classical system with a set of outcomes $\iota$, a state $\omega$ is pure if and only if there exists an outcome $i \in \iota$ such that $\omega$ is the deterministic state $\text{eval } i$, which maps an observable $A: \iota \to \mathbb{R}$ to its value at $i$, i.e., $\omega(A) = A(i)$.

For a finite classical system with a set of outcomes $\iota$, the algebraic state space is a simplex. This means that every state of the system can be uniquely represented as a convex combination (mixture) of its pure, deterministic states.

In the real numbers $\mathbb{R}$ (viewed as an Archimedean order-unit space), an effect $e$ (an element such that $0 \le e \le 1$) is sharp if and only if $e = 0$ or $e = 1$.