2 Matrices and operators in the Loewner order

The construction keeps a positive definite matrix above a multiple of the identity and a strictly positive operator, positive and invertible, above a multiple of the Gram operator, and controls each through one real number. This chapter collects what is needed about the Loewner order, the trace and rank-one updates, for matrices and for operators on a complex Hilbert space \(H\); for \(H = \mathbb {C}^{\iota }\) the operators are the matrices. Mathlib has no trace-class theory, so the trace of a positive operator is built here from a Hilbert basis.