5.1 The upper potential and the verifier

Definition 5.1 Upper potential and verifier of an operator

✓

Let \(H\) be a complex Hilbert space, let \(J\) be a positive injective operator on \(H\) of finite trace, let \(B\) be a strictly positive operator on \(H\), that is positive and invertible, and let \(\zeta {\gt} 0\). The upper potential of \(B\) is \(\Psi _J(B) = \operatorname {Tr}\bigl( J B^{-1} \bigr)\), and with \(X = (B + \zeta \cdot J)^{-1}\) the upper verifier at \(u \in H\) is

\[ U_B^{\zeta }(u) = \frac{\operatorname {Re}\langle u, X J X u \rangle }{\Psi _J(B) - \Psi _J(B + \zeta \cdot J)} + \operatorname {Re}\langle u, X u \rangle . \]

The upper potential is large when \(B\) is small in the directions where \(J\) is large. Before each step \(B\) is grown by \(\zeta \cdot J\), which lowers the potential by an amount that is computed exactly, and the verifier decides whether a candidate point stays within that budget, as \(\Phi \) and \(L_A^{\delta }\) do for the first family (Definition 4.1). A bound on the potential is a bound on the operator, \(\Psi _J(B)^{-1} \cdot J \preceq B\) (Lemma 2.7(c)). In Lean both notions are also defined directly for matrices (Discretization.upperPotential, Discretization.upperVerifier). Lean proves the next three lemmas a second time for matrices, where the trace is the matrix trace, and the read-off Lemma 5.5 once for every upper state; the matrix proofs serve the finite case and keep the sparsification theorem elementary.

Lemma 5.2 How the upper potential changes

✓

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\).

(a) For every \(\zeta \geq 0\) the operator \(B + \zeta \cdot J\) is strictly positive and

\[ \Psi _J(B) - \Psi _J(B + \zeta \cdot J) = \zeta \, \operatorname {Tr}\bigl( (J B^{-1} J) (B + \zeta \cdot J)^{-1} \bigr), \]

and for \(\zeta {\gt} 0\) the right-hand side is positive.

(b) Let \(C\) be a strictly positive operator on \(H\), let \(u \in H\), and let \(w \geq 0\) with \(w \operatorname {Re}\langle u, C^{-1} u \rangle {\lt} 1\). Then

\[ \Psi _J \bigl( C - w \, u u^* \bigr) = \Psi _J(C) + \frac{w}{1 - w \operatorname {Re}\langle u, C^{-1} u \rangle } \, \operatorname {Re}\langle u, C^{-1} J C^{-1} u \rangle . \]

Proof ▼

(a) The operator \(B + \zeta \cdot J\) dominates \(B\), so it is positive, and invertible because it dominates an invertible positive operator. The identity is the resolvent identity, which holds in any ring. The right-hand side is the trace of a product of two positive operators, the first of them \(J B^{-1} J\), which is again of finite trace and positive; Lemma 2.6(b) gives the sign, and injectivity of \(J\) makes it strict.

(b) Insert the Sherman–Morrison formula of Lemma 2.8(a) with \(t = -w\) and take traces, as for the lower potential in Lemma 4.2(b).

Lemma 5.3 Barrier lemma for the upper potential

✓

Let \(H\) be a nonzero complex Hilbert space, let \(J\) be a positive injective operator on \(H\) of finite trace, let \(B\) be a strictly positive operator on \(H\), let \(\zeta {\gt} 0\), \(u \in H\), and let \(w {\gt} 0\) satisfy \(U_B^{\zeta }(u) \leq 1/w\). Then \(B + \zeta \cdot J - w \, u u^*\) is strictly positive and

\[ \Psi _J \bigl( B + \zeta \cdot J - w \, u u^* \bigr) \leq \Psi _J(B). \]

Proof ▼

Write \(X = (B + \zeta \cdot J)^{-1}\). The first summand of \(U_B^{\zeta }(u)\) is positive for \(u \neq 0\), because \(\operatorname {Re}\langle u, X J X u \rangle = \| J^{1/2} X u\| ^2\) and \(J\) is injective, so the hypothesis gives \(w \operatorname {Re}\langle u, X u \rangle {\lt} 1\): the Sherman–Morrison denominator is positive, and Lemma 2.8(b), applied to the strictly positive operator \(B + \zeta \cdot J\) of Lemma 5.2(a), makes \(B + \zeta \cdot J - w \, u u^*\) strictly positive. Finally Lemma 5.2(b) for \(C = B + \zeta \cdot J\) and (a) reduce the inequality to the hypothesis \(U_B^{\zeta }(u) \leq 1/w\) multiplied out, as in the proof of Lemma 4.3.