2.4 From the trace of an inverse to the Loewner order
An operator is strictly positive if it is positive and invertible; this is Mathlib’s IsStrictlyPositive, and for a matrix it means positive definite. The inverse is Ring.inverse, defined on all operators and equal to the inverse on the invertible ones.
The next lemma is the reason the whole argument can be run on two real numbers: a bound on the trace of an inverse is a bound in the Loewner order. The traces \(\operatorname {Tr}A^{-1}\) and \(\operatorname {Tr}(J B^{-1})\) are the lower and the upper potential of Chapter 4 and Chapter 5.
(a) Let \(\iota \) be a finite set and let \(A \in \mathbb {C}^{\iota \times \iota }\) be positive definite. Then \(\bigl( \operatorname {Tr}A^{-1} \bigr)^{-1} \cdot 1 \preceq A\).
(b) If moreover \(0 {\lt} \delta {\lt} (\operatorname {Tr}A^{-1})^{-1}\), then \(A - \delta \cdot 1\) is positive definite.
(c) Let \(H\) be a nonzero complex Hilbert space, let \(J\) be a positive injective operator on \(H\) of finite trace, and let \(B\) be a strictly positive operator on \(H\). Then \(\operatorname {Tr}(J B^{-1}) {\gt} 0\) and
(a) Lemma 2.1(b) applied to \(A^{-1}\) gives \(A^{-1} \preceq (\operatorname {Tr}A^{-1}) \cdot 1\), and Lemma 2.1(d) turns that around.
(b) Write \(A - \delta \cdot 1 = \bigl( A - (\operatorname {Tr}A^{-1})^{-1} \cdot 1 \bigr) + \bigl( (\operatorname {Tr}A^{-1})^{-1} - \delta \bigr) \cdot 1\), a positive semidefinite matrix by (a) plus a positive definite one.
(c) The operator \(B^{-1/2} J B^{-1/2}\) is positive and of finite trace, and its trace is again \(\operatorname {Tr}(J B^{-1})\) by Lemma 2.6(b), which is positive since \(J \neq 0\) on the nonzero space \(H\). So Lemma 2.6(a) bounds it by \(\operatorname {Tr}(J B^{-1}) \cdot 1\), and Lemma 2.2 carries that back to \(J \preceq \operatorname {Tr}(J B^{-1}) \cdot B\). Lean proves (c) a second time for positive definite matrices, which is what the finite case uses.