1 The problem and the result
Let \((\Omega , \mu )\) be a measure space and \(\iota \) a finite nonempty index set with \(m = \# \iota \) elements. Two objects are given: a finite family \(a = (a_k)_{k \in \iota }\) of square-integrable functions on \(\Omega \), read as a map \(a : \Omega \to \mathbb {C}^{\iota }\), and a square-integrable map \(b : \Omega \to H\) into a separable complex Hilbert space \(H\). We ask whether the integral of \(|f|^2\) can be replaced by finitely many weighted point evaluations, so that the first family stays a frame from below and \(b\) stays a frame from above. A statement about weighted sums of \(|f(x_i)|^2\) is a statement about the matrix \(\sum _i w_i \, a(x_i) a(x_i)^*\) or the operator \(\sum _i w_i \, b(x_i) b(x_i)^*\), compared in the Loewner order: \(A \preceq B\) means that \(B - A\) is positive semidefinite. That is the form the argument takes.
The Gram operator of \(b\) is
a Bochner integral of the rank-one operators \(b(x) b(x)^* = \langle b(x), \cdot \rangle \, b(x)\) on \(H\). For \(H = \mathbb {C}^{\iota }\) it is a matrix, so the family \(a\) has the Gram matrix \(G(a)\), in Lean Discretization.gram. For \(\Lambda {\gt} 0\) with \(G(b) \preceq \Lambda \cdot 1\), the number \(M = \operatorname {Tr}G(b) / \Lambda \) is the effective dimension of \(G(b)\) relative to \(\Lambda \); it is at most \(\dim H\), and much smaller as soon as the eigenvalues of \(G(b)\) decay.
The following theorem is Theorem 3 of Chkifa, Dolbeault, Krieg and Ullrich [ 3 ] , for a second family with values in a separable Hilbert space. Its first bound is their factor \((1 - \sqrt{(m-1)/n})^2 \lambda _{\min }(I)\) in Loewner form.
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 \(I = G(a) = \int _\Omega a(x) a(x)^* \, d\mu (x)\) positive definite, let \(b : \Omega \to H\) be square-integrable, and let \(J = G(b) = \int _\Omega b(x) b(x)^* \, d\mu (x)\) be its Gram operator; assume that \(J\) is injective. Let \(\Lambda {\gt} 0\) satisfy \(J \preceq \Lambda \cdot 1\), and put \(m = \# \iota \) and \(M = \int _\Omega \| b(x)\| ^2 \, d\mu (x) / \Lambda \). Then for every \(n \geq m\) there are points \(x_1, \dots , x_n \in \Omega \) and weights \(w_1, \dots , w_n {\gt} 0\) with
in the matrix order and
in the order of operators.
The proof is given in Chapter 6, after the construction it rests on. No side condition on \(m\) or on \(M\) is needed; the potential argument there needs two, and three further cases of the proof remove them. Both hypotheses on \(J\) can be read on \(b\) (Lemma 3.2): \(J \preceq \Lambda \cdot 1\) is the bound \(\int _\Omega |\langle u, b \rangle |^2 \, d\mu \leq \Lambda \| u\| ^2\) for every \(u \in H\), and \(J\) is injective exactly when \(\langle u, b(\cdot ) \rangle = 0\) almost everywhere only for \(u = 0\).
A countable family \(b = (b_k)_{k \in \kappa }\) of square-integrable functions with \(\sum _k \| b_k\| _{L_2}^2 {\lt} \infty \) is the case \(H = \ell _2(\kappa )\) and \(b(x) = (b_k(x))_k\). The Gram operator is the Gram matrix \((\int _\Omega b_k \overline{b_l} \, d\mu )_{k,l}\), \(M = \sum _k \| b_k\| _{L_2}^2 / \Lambda \), and the upper bound reads \(\sum _i w_i |\sum _k c_k \, b_k(x_i)|^2 \leq (1 + \sqrt{(M-1)/n})^2 \Lambda \| c\| ^2\) for every \(c \in \ell _2(\kappa )\). Nothing pointwise is assumed: by Tonelli, \(\sum _k |b_k(x)|^2 {\lt} \infty \) almost everywhere, and the points are chosen there. This is the form of Theorem 3 of [ 3 ] ; in Lean it is Discretization.Countable.bss_generalized, and for finite \(\kappa \), proved with matrices, Discretization.bss_generalized. Read through quadratic forms, the lower bound is \((1 - \sqrt{(m-1)/n})^2 \int _\Omega |f|^2 \, d\mu \leq \sum _i w_i |f(x_i)|^2\) for \(f\) in the span of the first family; for finite \(\kappa \) both bounds in this form are Discretization.exists_discretization.
For \(b = a\), Theorem 1.1 gives the sparsification theorem of Batson, Spielman and Srivastava [ 1 ] in a slightly stronger form: \(\sqrt{(m-1)/n}\) in place of their \(\sqrt{m/n}\), which comes from [ 3 ] . Part (b) below is their statement for finitely many vectors, over \(\mathbb {C}\).
Let \(\iota \) be a finite nonempty set and put \(m = \# \iota \).
(a) Let \((\Omega , \mu )\) be a measure space 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\). Then for every \(n \geq m\) there are points \(x_1, \dots , x_n \in \Omega \) and weights \(w_1, \dots , w_n {\gt} 0\) with
(b) Let \(\Omega \) be a finite set and let \(v_k \in \mathbb {C}^{\iota }\), for \(k \in \Omega \), be vectors with \(\sum _{k \in \Omega } v_k v_k^* = 1\). Then for every \(n \geq m\) there are weights \(s_k \geq 0\), at most \(n\) of them nonzero, with
(a) This is Theorem 1.1 for \(b = a\), \(H = \mathbb {C}^{\iota }\) and \(I = 1\): the Gram operator of the second family is then the identity, \(\Lambda = 1\) bounds it, and its effective dimension is \(\operatorname {Tr}1 / 1 = m\), so both frame constants are built from the same \(r = \sqrt{(m-1)/n}\).
(b) The counting measure on \(\Omega \) has Gram matrix \(\sum _k v_k v_k^* = 1\), so (a) applies to \(k \mapsto v_k\). A vector chosen several times receives the sum of its weights, \(s_k = \sum _{i : x_i = k} w_i\), which leaves both sums unchanged, and a nonzero \(s_k\) belongs to one of the \(n\) chosen points.
Read through quadratic forms, with the kernel sections of a reproducing kernel Hilbert space as second family, the theorem becomes a statement about norms, Corollary 4 of [ 3 ] : the \(L_2\)-norm on the span of the first family is discretized from below, and the norm of the space from above.
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 positive definite Gram matrix \(I = \int _\Omega a(x) a(x)^* \, d\mu (x)\). Let \(H\) be a nonzero separable complex Hilbert space of measurable functions on \(\Omega \) on which every point evaluation is continuous, let \(K\) be its reproducing kernel, and assume \(\int _\Omega K(x, x) \, d\mu (x) {\lt} \infty \). Let \(\Lambda {\gt} 0\) satisfy \(\int _\Omega |g|^2 \, d\mu \leq \Lambda \| g\| _H^2\) for every \(g \in H\), and assume that the only \(g \in H\) vanishing almost everywhere is \(g = 0\). Put \(m = \# \iota \) and \(M = \int _\Omega K(x, x) \, d\mu (x) / \Lambda \). Then for every \(n \geq m\) there are points \(x_1, \dots , x_n \in \Omega \) and weights \(w_1, \dots , w_n {\gt} 0\) with
for every \(f \in \operatorname {span}\{ a_k\} \), and with
for every \(g \in H\).
Take for \(b(x)\) the kernel section \(k_x\) of Lemma 3.4: \(b\) is square-integrable, \(|\langle g, k_x \rangle | = |g(x)|\) and \(\| k_x\| ^2 = K(x, x)\). By Lemma 3.2(b) and (c) the two assumptions on \(H\) say that the Gram operator of \(b\) satisfies \(J \preceq \Lambda \cdot 1\) and is injective, and \(\int _\Omega \| b\| ^2 \, d\mu = \int _\Omega K(x, x) \, d\mu \), so Theorem 1.1 applies. Its two bounds are inequalities between quadratic forms. For \(f = \sum _k \overline{c_k} \, a_k\) one has \(\sum _i w_i |f(x_i)|^2 = c^* A c\) with \(A = \sum _i w_i \, a(x_i) a(x_i)^*\), and \(\int _\Omega |f|^2 \, d\mu = c^* I c\) by Lemma 3.1(a); this is the first bound. For \(g \in H\), \(\langle g, \sum _i w_i \, k_{x_i} k_{x_i}^* \, g \rangle = \sum _i w_i |\langle g, k_{x_i} \rangle |^2 = \sum _i w_i |g(x_i)|^2\); this is the second.
The first bound involves only the functions of the span, so the case \(I = 1\) already gives it: \(I^{-1/2} a\) spans the same space and has Gram matrix \(1\).
The constant \(\Lambda \) is the squared norm of the embedding \(H \hookrightarrow L_2(\mu )\), and the assumption on vanishing functions says that this embedding is injective.
Every square-integrable map \(b : \Omega \to H\) with injective Gram operator gives such a space: the functions \(\langle u, b(\cdot ) \rangle \), with norm \(\| u\| \) and kernel \(K(x, y) = \langle b(x), b(y) \rangle \), for which \(\int _\Omega K(x, x) \, d\mu = \int _\Omega \| b\| ^2 \, d\mu \). So the corollary covers every such \(b\); in Lean this form is Discretization.Infinite.exists_discretization.
On a probability space the lower bound of Theorem 1.1 holds with equal weights, a one-sided discretization of the \(L_2\)-norm. With equal weights and of the order of \(m\) points, Limonova and Temlyakov [ 6 , Theorem 1.1 ] prove such a discretization for spaces satisfying a Nikol’skii-type inequality, and Bartel, Schäfer and Ullrich [ 2 ] for arbitrary spaces, up to constants. The form below is the case \(p = 2\) of Proposition 8 of [ 3 ] , whose argument is followed here: for \(b \equiv 1\) in \(H = \mathbb {C}\) one has \(J = 1\) and \(\Lambda = M = 1\), and the upper bound \(\sum _i w_i \leq 1\) of the theorem comes, in the case \(M \leq 1 + 1/n\) of the proof, from a construction that bounds every single weight by \(1/n\).
Let \((\Omega , \mu )\) be a probability space, let \(\iota \) be a finite nonempty set with \(m = \# \iota \) elements, and let \(a : \Omega \to \mathbb {C}^{\iota }\) be square-integrable in every coordinate with \(I = \int _\Omega a(x) a(x)^* \, d\mu (x)\) positive definite. Then for every \(n \geq m\) there are points \(x_1, \dots , x_n \in \Omega \), not necessarily distinct, with
Put \(r = \sqrt{(m-1)/n}\). It suffices to find weights \(0 {\lt} w_i \leq 1/n\) with \((1 - r)^2 \cdot I \preceq \sum _i w_i \, a(x_i) a(x_i)^*\): the quadratic form of this inequality at the coefficient vector of \(f\) is \((1 - r)^2 \int _\Omega |f|^2 \, d\mu \leq \sum _i w_i |f(x_i)|^2\) by Lemma 3.1(a), and raising each \(w_i\) to \(1/n\) only enlarges the right-hand side. The first family is normalized as in the proof of Theorem 1.1, which leaves the weights unchanged, so let \(I = 1\).
For \(m \geq 2\), run the construction of the case \(M \leq 1 + 1/n\) in the proof of Theorem 1.1 with the constant upper verifier \(U \equiv n\), whose average is \(n\) because \(\mu \) is a probability measure. It starts from \(A_0 = (\delta m / r) \cdot 1\) with \(\delta = (1-r)/n\), tracks only the lower matrix with Lemma 4.3, finds each point with Lemma 4.4(b), and gives the lower bound by Lemma 4.5. Each point \(x_i\) satisfies \(U(x_i) {\lt} L(x_i)\) for the lower verifier \(L\) and receives the weight \(w_i = 1/L(x_i)\), so \(w_i \, n \leq 1\).
For \(m = 1\) the lower constant is \(1\). The lower verifier \(L(x) = n |a(x)|^2\) and \(U \equiv n\) have the same average \(n\), so Lemma 3.5(b) gives a point \(y\) with \(n \leq n |a(y)|^2\). Used \(n\) times with the weight \(1/(n |a(y)|^2) \leq 1/n\), it makes \(\sum _i w_i |a(x_i)|^2 = 1\).
In the Loewner order the corollary reads \((1 - \sqrt{(m-1)/n})^2 \cdot I \preceq \frac{1}{n} \sum _i a(x_i) a(x_i)^*\) (Discretization.bss_lower_equal_weights).