4.3 From the potential to the frame bound
Let \(\iota \) be a finite nonempty set, let \(n \geq 1\), and let \(v_1, \dots , v_n \in \mathbb {C}^{\iota }\) and \(w_1, \dots , w_n \in \mathbb {R}\). Let \(r {\gt} 0\) with \(r \neq 1\), put \(\delta = (1 - r)/n\) and \(c_0 = \delta (n r^2 + 1)/r\), and let \(A_n = c_0 \cdot 1 - n \delta \cdot 1 + \sum _{i=1}^n w_i \, v_i v_i^*\). If \(A_n\) is positive definite and \(\Phi (A_n) \leq r / \delta \), then
By Lemma 2.7(a), \(\Phi (A_n) \leq r/\delta \) gives \((\delta / r) \cdot 1 \preceq A_n\); inserting the definition of \(A_n\) gives \((\delta /r + n\delta - c_0) \cdot 1 \preceq \sum _i w_i \, v_i v_i^*\), and \(\delta /r + n\delta - c_0 = n \delta (1 - r) = (1 - r)^2\). The arithmetic is in Discretization/Parameters.lean.
For \(r = \sqrt{(m-1)/n}\) one has \(n r^2 + 1 = m\); the lemma is stated in \(r\) because its proof never unfolds the square root.