PhyslibAlpha.ProbabilisticTheory.JordanOrderUnit.Basic

Jordan order-unit spaces

i. Overview

Quantum observables carry, besides their order and unit, the Jordan product `a ∘ b`, a commutative product satisfying the Jordan identity. A Jordan order-unit space is an order-unit space that is a real Jordan algebra, using Mathlib's `IsCommJordan`, whose squares are nonnegative: `0 ≤ a ∘ a`. In the operator picture `⟪ψ, a² ψ⟫ = ‖a ψ‖² ≥ 0`.

ii. Key results

`IsJordanOrderUnit` : a Jordan order-unit space.
`IsJordanOrderUnit.sq_nonneg` : squares are nonnegative.

iii. Table of contents

A. The compatibility class
B. Consequences

A. The compatibility class

B. Consequences

1 declaration

theorem

Squares are non-negative in a Jordan order-unit space ( $0 \leq a^2$ )

#sq_nonneg

In a Jordan order-unit space $E$ , for any element $a \in E$ , its square is non-negative, satisfying $0 \leq a^2$ , where $a^2$ denotes the Jordan product of $a$ with itself.