Physlib

Physlib.ProbabilisticTheory.OrderUnit.Basic

Ordered vector spaces and order units

i. Overview

Order-unit spaces capture the basic structure needed for a probabilistic theory: observables, positivity, effects, states and probabilities. They do this without assuming that the theory is classical or quantum, or that observables have any particular algebraic structure.

In quantum mechanics, the standard example is the real vector space of self-adjoint matrices, ordered by positive semidefiniteness, with the identity matrix as 1. Keeping only the vector space, its order, and this distinguished unit gives the abstract order-unit setting.

ii. Key results

- `OrderUnitSpace.exists_two_sided_bound` : every observable sits between `-(n • 1)` and `n • 1`, for some `n`. - `OrderUnitSpace.exists_eq_sub_nonneg` : every observable is a difference of two positive observables. - `OrderUnitSpace.exists_real_shift_nonneg` : enough copies of the order unit shift any element into the positive cone. - `OrderedVectorSpace.nonneg_add_eq_zero` : the positive cone meets its negation only at `0`.

iii. Table of contents

  • A. Ordered vector spaces and order units
  • B. Consequences of being an order unit

iv. References

A. Ordered vector spaces and order-unit elements

B. Consequences of being an order unit

4 declarations

theorem

Every element AA is bounded by natural multiples of the order unit: −n⋅1≤A≤n⋅1-n \cdot 1 \le A \le n \cdot 1

In an order-unit space EE with a distinguished order unit 11, for every element A∈EA \in E, there exists a natural number n∈Nn \in \mathbb{N} such that AA is bounded on both sides by the nn-th natural multiple of the order unit: −n⋅1≤A≤n⋅1-n \cdot 1 \le A \le n \cdot 1 where ≤\le denotes the partial order of the space.

theorem

Every element AA can be written as A=Ap−AnA = A_p - A_n for some Ap,An≥0A_p, A_n \ge 0

For any element AA in an order-unit space EE, there exist elements Ap,An∈EA_p, A_n \in E such that 0≤Ap0 \le A_p, 0≤An0 \le A_n, and A=Ap−AnA = A_p - A_n.

theorem

Every element AA can be shifted by r⋅1r \cdot 1 to be non-negative (r⋅1+A≥0r \cdot 1 + A \ge 0)

In an order-unit space EE with a distinguished order unit 11, for every element A∈EA \in E, there exists a real number r∈Rr \in \mathbb{R} such that the element AA shifted by the scalar multiple r⋅1r \cdot 1 is non-negative: 0≤r⋅1+A0 \le r \cdot 1 + A This reflects the property that every observable can be shifted into the positive cone by adding a sufficiently large multiple of the order unit.

theorem

If A,B≥0A, B \ge 0 and A+B=0A + B = 0, then A=0A = 0

Let EE be an ordered vector space. For any non-negative elements A,B∈EA, B \in E (where A≥0A \ge 0 and B≥0B \ge 0), if their sum A+B=0A + B = 0, then A=0A = 0. Geometrically, this means the positive cone of the vector space meets its negation only at the zero vector.