PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.Order

The positive cone of a JB-algebra

i. Overview

In an ordered JB-algebra the nonnegative observables are exactly the squares: every nonnegative observable is a square in its closed one-generator subalgebra.

ii. Key results

`JBAlgebra.nonneg_iff_exists_mul_self` : the nonnegative observables are the squares.

1 declaration

theorem

$0 \le a \iff \exists b, a = b^2$ in JB-algebras

#nonneg_iff_exists_mul_self

Let $E$ be a JB-algebra. For any element $a \in E$ , $a$ is non-negative ( $0 \le a$ ) if and only if there exists an element $b \in E$ such that $a = b^2$ , where $b^2$ is the Jordan product $b * b$ .

PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.JB.Order

The positive cone of a JB-algebra

i. Overview

ii. Key results

0≤a ⟺ ∃b,a=b20 \le a \iff \exists b, a = b^20≤a⟺∃b,a=b2 in JB-algebras

$0 \le a \iff \exists b, a = b^2$ in JB-algebras