LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A proper matrix-product cover from the mixed (2,1) norm

Statement

Let $X \in R^{n \times d}$ , $M \in R^{d \times m}$ with $n, d, m \geq 1$ , and let $a, s \geq 0$ . Suppose $C : = {A \in R^{d \times m} : ∥ A - M ∥_{2, 1} \leq a, ∥ A ∥_{σ} \leq s}$ is nonempty. Put $U : = {X A : A \in C}$ . For every $ϵ > 0$ , $\log N_{F} (U, ϵ) \leq 5 \frac{a^{2} ∥ X ∥_{F}^{2}}{ϵ^{2}} \log (2 d m) .$ If $a ∥ X ∥_{F} = 0$ or $ϵ \geq 2 a ∥ X ∥_{F}$ , then $N_{F} (U, ϵ) = 1$ . Here $∥ A - M ∥_{2, 1}$ is the sum of the Euclidean norms of the columns of $A - M$ ; when applying this lemma to a network layer, take $A = A_{i}^{⊤}$ and $M = M_{i}^{⊤}$ , as in the spectral-network-complexity definition. The number $N_{F}$ is the proper Frobenius covering number.

Statement references

Spectral network complexity with reference matrices: defines the column-sum mixed norm and the induced Euclidean operator norm.

Proper Frobenius covering numbers: defines the proper cover whose centers must lie in $U$ .

The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices: defines the Euclidean matrix-entry norm used to measure cover error.

Bartlett, Foster, and Telgarsky, Lemma 3.2 and Appendix A.4: gives the Maurey sparsification route to this matrix-product cover.

Facts & Assumptions

Given: Matrices $X, M$ , dimensions and constants as in the Statement, and the nonempty feasible set $C$ .

[F1]

$∥ Z ∥_{F}^{2}$ is the sum of the squared absolute values of all entries of $Z$ . The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices

[F2]

$∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ in a real or complex inner-product space. Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors

[F3]

The Euclidean inner-product norm is homogeneous and satisfies the triangle inequality. The inner-product norm is definite, homogeneous, and satisfies the triangle inequality

[F4]

$N_{F} (U, ϵ)$ is the least size of a finite proper Frobenius cover of $U$ . Proper Frobenius covering numbers

[F5]

Closed bounded subsets of finite-dimensional real Euclidean space are compact. Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line

[F6]

$\log$ is strictly increasing on positive reals and satisfies $\log (x y) = \log x + \log y$ . The natural logarithm as the inverse of the exponential function Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

[F7]

The mixed norm is the sum of the Euclidean column norms, and $∥ A ∥_{σ}$ is the induced Euclidean operator norm. Spectral network complexity with reference matrices

[F8]

A continuous map from a compact metric space has compact image. The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset

[F9]

A continuous real-valued function on a nonempty compact metric space attains its minimum. A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value

Proof

1.1F1F2F7givenalgebra

For any $B \in R^{d \times m}$ , write its columns as $b_{j}$ and the columns of $X$ as $x_{r}$ . By [F2], $∥ X b_{j} ∥_{2}^{2} = \sum_{i} ∣ \sum_{r} X_{i r} (b_{j})_{r} ∣^{2} \leq ∥ X ∥_{F}^{2} ∥ b_{j} ∥_{2}^{2}$ . Summing over $j$ gives $∥ X B ∥_{F} \leq ∥ X ∥_{F} (\sum_{j} ∥ b_{j} ∥_{2}^{2})^{1 / 2} \leq ∥ X ∥_{F} \sum_{j} ∥ b_{j} ∥_{2} = ∥ X ∥_{F} ∥ B ∥_{2, 1}$ ; the middle inequality follows by squaring, since all column norms are nonnegative. Thus $∥ A - A^{'} ∥_{2, 1} \leq 2 a$ for $A, A^{'} \in C$ , and the diameter of $U$ is at most $2 a ∥ X ∥_{F}$ . If $a ∥ X ∥_{F} = 0$ , $U$ is a singleton; if $ϵ \geq 2 a ∥ X ∥_{F}$ , any one point of nonempty $U$ covers it.

1.2F1F2F7givenconstructalgebra

Assume $a ∥ X ∥_{F} > 0$ and $0 < ϵ < 2 a ∥ X ∥_{F}$ . For each nonzero column $x_{r}$ , each output coordinate $j$ , and each sign $η \in {- 1, + 1}$ , form the rank-one atom $V_{r j η} = η (x_{r} / ∥ x_{r} ∥_{2}) e_{j}^{⊤}$ , where $e_{j}$ is the $j$ th standard basis vector in $R^{m}$ . There are at most $2 d m$ atoms and each has Frobenius norm $1$ . For $B = A - M$ , the expansion $X B = \sum_{r, j} (B)_{r j} x_{r} e_{j}^{⊤}$ has coefficient mass $β : = \sum_{r, j} ∣ B_{r j} ∣ ∥ x_{r} ∥_{2} \leq ∥ B ∥_{2, 1} ∥ X ∥_{F} \leq a ∥ X ∥_{F} = : c$ , by [F2] column by column. Hence $X B / c$ lies in the convex hull of these signed atoms: if $β < c$ , fill the remaining weight with $0$ , which is the midpoint of an atom and its negative. If $β = 0$ , the product is $0$ .

2.1F1step 1.2givenalgebraconstruct

For an integer $k \geq 1$ , sample $k$ atoms independently from the finite convex representation of $X B / c$ constructed in step 1.2. If $V_{1}, \dots, V_{k}$ are these atoms and $E V_{1} = X B / c$ , expansion of the squared Frobenius norm and independence give $E ∥ c k^{- 1} \sum_{t = 1}^{k} V_{t} - X B ∥_{F}^{2} = (c^{2} / k) (E ∥ V_{1} ∥_{F}^{2} - ∥ E V_{1} ∥_{F}^{2}) \leq c^{2} / k$ . Therefore some ordered $k$ -tuple gives a center within $c / \sqrt{k}$ , and all such centers number at most $(2 d m)^{k}$ . Taking $k = ⌈ c^{2} / ϵ^{2} ⌉$ yields an external $ϵ$ -cover of the translated relaxed product set $X M + {X B : ∥ B ∥_{2, 1} \leq a}$ .

3.1F1F2F3F5F7F8F9step 1.1step 2.1givenalgebraconstruct

The mixed-norm constraint set is convex: for $A, A^{'} \in C$ and $0 \leq t \leq 1$ , the column triangle inequality [F3] gives $∥ t (A - M) + (1 - t) (A^{'} - M) ∥_{2, 1} \leq t a + (1 - t) a = a$ . The operator-norm constraint is convex because for each unit vector $v$ , $∥ (t A + (1 - t) A^{'}) v ∥_{2} \leq t ∥ A v ∥_{2} + (1 - t) ∥ A^{'} v ∥_{2} \leq s$ , and taking the supremum over $v$ preserves the bound. The mixed norm is continuous as a finite sum of continuous column norms. From [F7] and the Euclidean triangle inequality, $∣ ∥ A ∥_{σ} - ∥ A^{'} ∥_{σ} ∣ \leq ∥ A - A^{'} ∥_{σ} \leq ∥ A - A^{'} ∥_{F}$ , where the last inequality follows from the rowwise Cauchy estimate in step 1.1; hence the operator norm is continuous and $C$ is closed. Also $∥ A - M ∥_{F} \leq ∥ A - M ∥_{2, 1} \leq a$ , so $C$ is bounded. Identify the real matrix space with $R^{d m}$ by its entries; its Euclidean norm is the Frobenius norm, so [F5] makes $C$ compact. The map $T (A) = X A$ is continuous because step 1.1 and [F2] give $∥ T (A) - T (A^{'}) ∥_{F} \leq ∥ X ∥_{F} ∥ A - A^{'} ∥_{2, 1} \leq \sqrt{m} ∥ X ∥_{F} ∥ A - A^{'} ∥_{F}$ . Hence [F8] makes $U = T (C)$ compact; it is convex because $C$ is convex and $T$ is linear. For each of the finitely many external centers $z$ from step 2.1, the function $u \mapsto ∥ z - u ∥_{F}$ is continuous on the nonempty compact metric space $U$ , since the reverse triangle inequality bounds its change by $∥ u - u^{'} ∥_{F}$ . Thus [F9] gives a nearest point $p \in U$ for each center; enumerate the finite center set and choose these minimizers successively. For any $u \in U$ , convexity gives $p + t (u - p) \in U$ for $0 \leq t \leq 1$ . Put $⟨ P, Q ⟩_{F} : = \sum_{i, j} P_{i j} Q_{i j}$ . Minimality implies $0 \leq ∥ z - p - t (u - p) ∥_{F}^{2} - ∥ z - p ∥_{F}^{2} = - 2 t ⟨ z - p, u - p ⟩_{F} + t^{2} ∥ u - p ∥_{F}^{2}$ for $0 < t \leq 1$ ; division by $t$ and passage to $t ↓ 0$ give $⟨ z - p, u - p ⟩_{F} \leq 0$ . Expanding $∥ z - u ∥_{F}^{2}$ then gives $∥ p - u ∥_{F}^{2} \leq ∥ z - u ∥_{F}^{2}$ . Thus projection does not increase distance to any point of $U$ , and the cover becomes proper without increasing its size.

4.1F4F6step 1.1step 3.1step 2.1algebra∎

Put $q = a^{2} ∥ X ∥_{F}^{2} / ϵ^{2} > 1 / 4$ . Then $k = ⌈ q ⌉ \leq q + 1 \leq 5 q$ , so step 2.1 and [F6] imply $\log N_{F} (U, ϵ) \leq k \log (2 d m) \leq 5 q \log (2 d m)$ . Together with step 1.1 this proves both cases of the Statement.

Depends on

Used by

Spectral and reference-matrix covering entropy for network outputs Lemma

Dependency tree · two levels

63 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Peter L. Bartlett, Dylan J. Foster, and Matus Telgarsky, Spectrally-normalized margin bounds for neural networks, Lemma 3.2 and Appendix A.4 (standard reference, not scraped)