PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JBW.Basic

Let $E$ be a JBW-algebra and $\omega$ be a normal state on $E$. If $(x_n)_{n \in \mathbb{N}}$ is a monotone increasing sequence in $E$ that is bounded above, then there exists an element $a \in E$ such that $a$ is the least upper bound of the range of the sequence $(a = \sup_{n} x_n)$, and $\omega(a)$ is the least upper bound of the set of values $\{\omega(x_n) \mid n \in \mathbb{N}\}$ (i.e., $\omega(a) = \sup_{n} \omega(x_n)$).

Let $E$ be a JBW-algebra and $\omega$ be a normal state on $E$. If $(x_n)_{n \in \mathbb{N}}$ is a monotone increasing sequence in $E$ that is bounded above, then the value of the state applied to the supremum of the sequence, $\omega(\sup_{n \in \mathbb{N}} x_n)$, is the least upper bound of the set of values $\{\omega(x_n) \mid n \in \mathbb{N}\}$.

Let $E$ be a JBW-algebra. For any non-zero element $x$ in the positive cone of $E$ (that is, $x \ge 0$ and $x \neq 0$), there exists a normal finite weight $w$ on $E$ such that $w(x) \neq 0$. Here, a weight is called finite if it maps all positive elements to finite values, and normal if it preserves the least upper bounds of monotone functions.