PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Observable

Given an additive group $A$ equipped with an additive involution $\ast$, the type `Observable A` represents the collection of self-adjoint elements of $A$, defined as those $a \in A$ such that $a^* = a$.

In an additive group $A$ equipped with an additive involution $\ast$ and a partial order $\le$, a positive observable is an element $a \in A$ that is both self-adjoint ($a^* = a$) and non-negative ($a \ge 0$).

Let $A$ be a space with an involution and $\omega \in \mathcal{S}[\mathbb{C}, A]$ be a complex-valued state (a unital positive linear map from $A$ to $\mathbb{C}$). The definition `onObservables` maps $\omega$ to a real-valued state on the space of observables of $A$, denoted as $\mathcal{S}[\mathbb{R}, \text{Observable } A]$. This induced state represents the expectation-value functional such that for any self-adjoint element $a \in \text{Observable } A$, the result is the real number $\omega(a)$.

Let $A$ be a space with an involution. For any complex-valued state $\omega \in \mathcal{S}[\mathbb{C}, A]$ and any observable $a \in \text{Observable } A$, the value of the induced real state $\omega.\text{onObservables}$ applied to $a$ is equal to the value of the original state $\omega$ applied to $a$ when the real result is cast to a complex number. That is, $$(\omega.\text{onObservables}(a) : \mathbb{C}) = \omega(a)$$ where $\omega.\text{onObservables} \in \mathcal{S}[\mathbb{R}, \text{Observable } A]$ is the real-valued state representing the expectation-value functional.