6.1 The barrier iteration
Let \((\Omega , \mu )\) be a measure space, let \(\iota \) be a finite nonempty set, and let \(H\) be a nonzero separable complex Hilbert space. Let \(a : \Omega \to \mathbb {C}^{\iota }\) be square-integrable in every coordinate with \(\int _\Omega a(x) a(x)^* \, d\mu (x) = 1\), and let \(b : \Omega \to H\) be square-integrable with injective Gram operator \(J = \int _\Omega b(x) b(x)^* \, d\mu (x)\). Let \(A_0 \in \mathbb {C}^{\iota \times \iota }\) be positive definite, let \(B_0\) be a strictly positive operator on \(H\), and let \(\delta , \zeta {\gt} 0\) satisfy the initial gap condition
For points \(x_1, \dots , x_k \in \Omega \) and weights \(w_1, \dots , w_k\) write
Then for every \(k \geq 0\) there are points \(x_1, \dots , x_k \in \Omega \) and weights \(w_1, \dots , w_k {\gt} 0\) such that \(A_k\) is positive definite, \(B_k\) is strictly positive, \(\Phi (A_k) \leq \Phi (A_0)\) and \(\Psi _J(B_k) \leq \Psi _J(B_0)\).
Induction on \(k\); for \(k = 0\) there is nothing to show. The invariant keeps the gap open, \(1/\zeta + \Psi _J(B_k) \leq 1/\zeta + \Psi _J(B_0) \leq 1/\delta - \Phi (A_0) \leq 1/\delta - \Phi (A_k)\), and in particular \(\delta {\lt} \Phi (A_k)^{-1}\). By Lemma 5.4 the function \(U(x) = U_{B_k}^{\zeta }(b(x))\) is integrable with average below \(1/\zeta + \Psi _J(B_k)\), so Lemma 4.4(b) produces a point \(x_{k+1}\) with \(U(x_{k+1}) {\lt} L_{A_k}^{\delta }(a(x_{k+1}))\). The weight is \(w_{k+1} = 1 / L_{A_k}^{\delta }(a(x_{k+1}))\), positive because \(U \geq 0\), and Lemma 4.3 and Lemma 5.3 restore the invariant.
The number of steps is arbitrary; only the initial gap condition drives it. What ties the number of points to the frame bounds is the choice of the initial states and of the two shifts, made in the proof of Theorem 1.1 below.
The induction and the read-off use only a few properties of the upper state: that \(\Psi _J(B)\) and \(U_B^{\zeta }\) are positive, Lemma 5.3 and Lemma 5.4, the bound \(\Psi _J(B)^{-1} \cdot J \preceq B\) (Lemma 2.7(c)) with the potential of a multiple of the identity, and the crude bound \(b(y) b(y)^* \preceq \| b(y)\| ^2 \cdot 1\) with \(\int _\Omega \| b\| ^2 \, d\mu = \operatorname {Tr}J\). In Lean they are collected in Discretization.UpperBarrier, and the construction, the read-off of the upper frame bound and the theorem with its edge cases are proved once for every such upper state. The operators of Chapter 5 are one instance (Discretization.Infinite.operatorUpperBarrier); the matrices over a finite set \(\kappa \), with the matrix proofs of the upper lemmas, are another (Discretization.matrixUpperBarrier).