First, some design has a positive definite Gram matrix (Discretization.KieferWolfowitz.exists_design_posDef). Linear independence of the coordinate functions says that \(c = 0\) is the only coefficient vector with \(\langle c, a(y) \rangle = 0\) for all \(y \in \Omega \). It therefore suffices to find points annihilating no nonzero coefficient vector, for then the uniform distribution on them has \(c^* G c {\gt} 0\) for every \(c \neq 0\) by the formula for \(c^* G c\). Descending induction on dimension supplies them: while some nonzero vector survives the points chosen so far, the hypothesis gives a point at which it does not vanish, and adding that point lowers the dimension.

The determinants of the Gram matrices of designs form a set of real numbers which is bounded above, since the entries of every Gram matrix are bounded by \(C^2\) and the Leibniz formula bounds a determinant by its entries, and which contains a positive number by the first step. Let \(S\) be its supremum and take a design whose determinant exceeds \(S / (1 + \eta )\), where \(\eta = \varepsilon ^2 / (4m(m + \varepsilon - 1))\); its Gram matrix \(G\) is positive definite because its determinant is positive.

Appending a point \(y\) with weight \(\alpha \in [0,1)\) and scaling the old weights by \(1 - \alpha \) is again a design, with Gram matrix \((1-\alpha ) G + \alpha \, a(y) a(y)^*\). By Lemma 2.9 its determinant is \(\det G\) multiplied by \((1-\alpha )^{m-1}(1 + \alpha (t-1))\) with \(t = a(y)^* G^{-1} a(y)\), and that multiple cannot exceed \(S / \det G {\lt} 1 + \eta \). If \(t\) were larger than \(m + \varepsilon \), the weight of Lemma 7.6 would make it at least \(1 + \eta \).

By Bernoulli’s inequality \((1-\alpha )^{m-1} \geq 1 - (m-1)\alpha \), and the difference of the two sides of the claim is then the explicit nonnegative quantity \((t-m)^2 / (4m^2(t-1))\). The weight \(\alpha \) is the one for which the linear gain \(\alpha (t-m)\) is twice the quadratic loss \((m-1)(t-1)\alpha ^2\), so half of the gain survives.

The Gram matrix lies in the convex hull of the matrices \(a(y) a(y)^*\), so by Carathéodory’s theorem it is a convex combination of affinely independent ones. These matrices are Hermitian, and the Hermitian matrices in \(\mathbb {C}^{\iota \times \iota }\) form a real vector space of dimension \(m^2\), since every complex matrix is uniquely \(H + iK\) with \(H\) and \(K\) Hermitian. An affinely independent family in it has at most \(m^2 + 1\) members.

Take the design of Proposition 7.5 for \(\varepsilon /2\). For \(s = m + \varepsilon \) the bound \(s^{-1} a(y)^* G^{-1} a(y) {\lt} 1\) is strict, so subtracting \(s^{-1} a(y) a(y)^*\) from \(G\) leaves a positive definite matrix by Lemma 2.8(b), that is \(a(y) a(y)^* \preceq s \cdot G\). Evaluating this at the coefficient vector \(c\) of \(f\), with \(c^* G c = \sum _k w_k |f(x_k)|^2\), gives \(|f(y)|^2 \leq s \sum _k w_k |f(x_k)|^2\). This inequality depends on the design only through its Gram matrix, which Lemma 7.7 preserves while cutting the design down to \(m^2 + 1\) points. Read as the measure \(\varrho = \sum _k w_k \delta _{x_k}\), the design gives the theorem: integration against \(\varrho \) is the weighted sum over the points, for every measurable integrand.

For \(\varepsilon = 0\) on a compact space, the matrices \(a(y) a(y)^*\) form a compact set, whose convex hull is compact as well and consists exactly of the Gram matrices of designs. The determinant is continuous, so it attains its maximum at a design. No mixture can then increase the determinant at all, and Lemma 7.6 applied with the factor \(1\) gives \(a(y)^* G^{-1} a(y) \leq m\) without slack. The passage to the norm inequality is the one above for every constant \(s {\gt} m\), followed by the limit \(s \to m\), which is a limit of real numbers, and the point count is again Lemma 7.7.

In Lean the design form is Discretization.KieferWolfowitz.exists_optimal_design_card_le and its compact counterpart, and Discretization.KieferWolfowitz.exists_measure_of_design turns a design into the measure.