6.2 Proof of the discretization theorem
The first family is normalized first. Replace \(a\) by \(I^{-1/2} a\), whose Gram matrix is \(I^{-1/2} I \, I^{-1/2} = 1\) by Lemma 3.1(b). Once points and weights are found for it, conjugating the lower bound by \(I^{1/2}\) preserves the Loewner order and turns \((1 - r)^2 \cdot 1\), with \(r = \sqrt{(m-1)/n}\), into \((1 - r)^2 \cdot I\); the upper bound does not involve the first family. From now on \(\int _\Omega a(x) a(x)^* \, d\mu (x) = 1\).
By Lemma 3.2(a) and Lemma 3.3(a), \(J\) is positive and of finite trace with \(\operatorname {Tr}J = \int _\Omega \| b\| ^2 \, d\mu = M \Lambda \), so the upper potential and verifier of Definition 5.1 are defined. Put \(r = \sqrt{(m-1)/n}\), so that \(n r^2 + 1 = m\), and for \(M \geq 1\) put \(s = \sqrt{(M-1)/n}\), so that \(n s^2 + 1 = M\).
Case \(m \geq 2\), \(M \geq 1 + 1/n\) (Discretization.bss_generalized_of_gram_eq_one), the potential argument. Put
Since \(2 \leq m \leq n\) we have \(0 {\lt} r {\lt} 1\), and \(M \geq 1 + 1/n\) gives \(s \geq 1/n\). Then \(\Phi (A_0) = r/\delta \) and \(\Psi _J(B_0) = s/\zeta \), so the initial gap closes exactly, \(1/\delta - \Phi (A_0) = n = 1/\zeta + \Psi _J(B_0)\). Proposition 6.1 with \(k = n\) gives points and weights with \(\Phi (A_n) \leq r/\delta \) and \(\Psi _J(B_n) \leq s/\zeta \), and Lemma 4.5 and Lemma 5.5 turn them into the two bounds. The remaining three cases need one potential only: the verifier on the other side is replaced by a constant, whose average is again \(n\). For \(m = 1\) the lower constant \((1 - r)^2\) is \(1\).
Case \(m = 1\), \(M \geq 1 + 1/n\) (Discretization.bss_generalized_of_unique). The lower verifier is replaced by \(L(x) = n |a(x)|^2\), whose average is \(n\) because the single function is normalized. The induction then tracks only the upper state, using Lemma 5.3 and the average of Lemma 5.4 with Lemma 3.5(a), and takes the largest weight the constant allows, \(1/w_i = L(x_i)\). Each point therefore contributes exactly \(1/n\) to the lower bound, which becomes the identity \(\sum _i w_i |a(x_i)|^2 = 1\). The upper bound is Lemma 5.5.
Case \(m \geq 2\), \(M \leq 1 + 1/n\) (Discretization.bss_generalized_of_small_dim). The upper verifier is replaced by \(U(x) = n \| b(x)\| ^2 / \operatorname {Tr}J\), whose average is \(n\). The induction tracks only the lower matrix, with Lemma 4.3, and the lower bound is Lemma 4.5. The weights it produces satisfy \(w_i U(x_i) \leq 1\), that is \(w_i \| b(x_i)\| ^2 \leq \operatorname {Tr}J / n\). Summing over the \(n\) points and using Lemma 2.8(c) gives \(\sum _i w_i \, b(x_i) b(x_i)^* \preceq \operatorname {Tr}J \cdot 1 = M \Lambda \cdot 1\), and \(M \leq 1 + 1/n\) forces \(s = \sqrt{(M-1)/n} \leq 1/n\) and hence \(M = 1 + n s^2 \leq 1 + s \leq (1+s)^2\).
Case \(m = 1\), \(M \leq 1 + 1/n\) (Discretization.bss_generalized_of_unique_of_small_dim). Both verifiers are now the constants \(L(x) = n |a(x)|^2\) and \(U(x) = n \| b(x)\| ^2 / \operatorname {Tr}J\), of equal average \(n\), and neither depends on the state of the construction. Lemma 3.5(b) produces a single point \(y\) with \(U(y) \leq L(y)\) and \(L(y) {\gt} 0\); using it \(n\) times with the weight \(w = 1/L(y)\) makes the lower bound the identity \(\sum _i w_i |a(x_i)|^2 = 1\), while \(w \, U(y) \leq 1\) and Lemma 2.8(c) give the upper bound as in the previous case. No induction is needed.
In Lean the normalisation is Discretization.bss_of_gram_eq_one, stated once for an arbitrary conclusion about the second family, and the four cases are proved once for every upper state of Discretization.UpperBarrier. A finite second family, \(H = \mathbb {C}^{\kappa }\), is proved with the matrix instance, which keeps Corollary 1.3 free of operators.