4.2 The verifier passes on average
A point may be used if the upper verifier stays below the lower one. Such a point exists because the lower verifier is large on average.
Let \((\Omega , \mu )\) be a measure space, let \(\iota \) be a finite nonempty set, and let \(a : \Omega \to \mathbb {C}^{\iota }\) be square-integrable in every coordinate with \(\int _\Omega a(x) a(x)^* \, d\mu (x) = 1\). Let \(A \in \mathbb {C}^{\iota \times \iota }\) be positive definite and \(0 {\lt} \delta {\lt} \Phi (A)^{-1}\).
(a) The lower verifier satisfies
(b) Let \(U : \Omega \to \mathbb {R}\) be integrable with \(\int _\Omega U \, d\mu \leq 1/\delta - \Phi (A)\). Then there is an \(x \in \Omega \) with \(U(x) {\lt} L_A^{\delta }\bigl( a(x) \bigr)\).
(a) Write \(Y = A^{-1}\) and \(Z = (A - \delta \cdot 1)^{-1}\). Lemma 3.1(a) turns the average into \(\operatorname {Tr}(Z^2) / (\delta \operatorname {Tr}(Y Z)) - \operatorname {Tr}Z\), the denominator being the gain of Lemma 4.2(a). Writing \(t = \operatorname {Tr}(Y Z)\) and \(u = \operatorname {Tr}(Y Z^2)\), the claim reduces to \(\delta t^2 {\lt} u\), which is what Lemma 2.3(b) gives together with \(\delta \Phi (A) {\lt} 1\).
(b) The lower verifier is a quadratic form in \(a(x)\) and hence integrable. By (a) its average exceeds \(1/\delta - \Phi (A) \geq \int _\Omega U \, d\mu \), and Lemma 3.5(a) gives the point.
In the construction \(U\) is the upper verifier along the second family, whose average is below \(1/\zeta + \Psi _J(B)\) by Lemma 5.4; the gap condition \(1/\zeta + \Psi _J(B) \leq 1/\delta - \Phi (A)\) then makes (b) applicable. Any weight \(w\) between the two reciprocals is admissible for Lemma 4.3 and for Lemma 5.3, and the construction takes the largest one, \(w = 1/L_A^{\delta }\). Part (b) compares two averages of real functions and nothing else; in Lean it is proved once for every upper state, Discretization.UpperBarrier.exists_admissible_point.