5.3 From the upper potential to the frame bound
Let \(H\) be a nonzero complex Hilbert space, let \(J\) be a positive injective operator on \(H\) of finite trace, let \(\Lambda {\gt} 0\) with \(J \preceq \Lambda \cdot 1\), let \(n \geq 1\), let \(s \geq 1/n\) with \(\operatorname {Tr}J = \Lambda (n s^2 + 1)\), put \(\zeta = (1 + s)/n\) and \(d_0 = \zeta \operatorname {Tr}J / s\), let \(u_1, \dots , u_n \in H\) and \(w_1, \dots , w_n \in \mathbb {R}\), and let \(B_n = d_0 \cdot 1 + n \zeta \cdot J - \sum _{i=1}^n w_i \, u_i u_i^*\). If \(B_n\) is strictly positive and \(\Psi _J(B_n) \leq s / \zeta \), then
By Lemma 2.7(c), \(\Psi _J(B_n) \leq s/\zeta \) gives \((\zeta / s) \cdot J \preceq B_n\), hence \(\sum _i w_i \, u_i u_i^* \preceq d_0 \cdot 1 + (n\zeta - \zeta /s) \cdot J\). The coefficient \(n\zeta - \zeta /s = \zeta (n - 1/s)\) is nonnegative exactly because \(s \geq 1/n\), so \(J \preceq \Lambda \cdot 1\) may be applied to it, and \(d_0 + (n\zeta - \zeta /s)\Lambda = \zeta \Lambda (n s + n) = (1 + s)^2 \Lambda \). In Lean this read-off is proved once for every upper state, Discretization.UpperBarrier.upper_bound_of_state; the arithmetic is in Discretization/Parameters.lean.
For \(s = \sqrt{(M-1)/n}\) one has \(n s^2 + 1 = M\), and \(s \geq 1/n\) is the condition \(M \geq 1 + 1/n\); the lemma is stated in \(s\) because its proof never unfolds the square root.