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.

Spectral and reference-matrix covering entropy for network outputs

Statement

Fix an architecture and activations as in the spectral-network-complexity definition, with widths $d_{0}, \dots, d_{L}$ and $W : = \max_{0 \leq i \leq L} d_{i}$ . Let $n \geq 1$ and let $X \in R^{n \times d_{0}}$ be any sample matrix. Let $M_{i} \in R^{d_{i} \times d_{i - 1}}$ , and fix $s_{i} > 0$ and $b_{i} \geq 0$ . Suppose each feasible layer set $C_{i} : = {A_{i} : ∥ A_{i} ∥_{σ} \leq s_{i}, ∥ A_{i}^{⊤} - M_{i}^{⊤} ∥_{2, 1} \leq b_{i}}$ is nonempty. Let $H_{X}$ be the set of $n \times d_{L}$ score matrices whose $r$ th row is $F_{A} (x_{r})^{⊤}$ , for $A_{i} \in C_{i}$ and the $r$ th row $x_{r}^{⊤}$ of $X$ . Then for every $ϵ > 0$ , $\log N_{F} (H_{X}, ϵ) \leq 5 \frac{∥ X ∥_{F}^{2}}{ϵ^{2}} \log (2 W^{2}) (\prod_{i = 1}^{L} (ρ_{i} s_{i})^{2}) {(\sum_{i = 1}^{L} (b_{i} / s_{i})^{2 / 3})}^{3} .$ The logarithm is natural, an empty product equals $1$ , and $N_{F}$ uses proper centers in the covered score-matrix set.

Statement references

Spectral network complexity with reference matrices: fixes the network recurrence, zero-origin Lipschitz activations, spectral norm, and mixed column-sum norm.

Proper Frobenius covering numbers: defines proper covers and their Frobenius radius.

A proper matrix-product cover from the mixed (2,1) norm: supplies the proper product cover for a fixed input matrix and one constrained layer.

Facts & Assumptions

Given: The architecture, activations, matrices, positive spectral bounds, nonnegative reference-distance bounds, nonempty layer sets, and sample matrix in the Statement.

[F1]

Each activation fixes zero and is $ρ_{i}$ -Lipschitz in Euclidean norm; each layer matrix has induced Euclidean norm at most $s_{i}$ , and its transpose-difference from the reference has column-sum norm at most $b_{i}$ . Spectral network complexity with reference matrices

[F2]

For a fixed input matrix $Z$ , the one-layer image under a nonempty feasible matrix set has a proper Frobenius cover satisfying the stated matrix-product entropy estimate. A proper matrix-product cover from the mixed (2,1) norm

[F3]

The Frobenius norm is the Euclidean norm of all matrix entries, so rowwise application of a $ρ_{i}$ -Lipschitz map changes Frobenius distances by at most the factor $ρ_{i}$ . The Frobenius norm $∥ A ∥_{F} = (\sum_{i, j} ∣ a_{i j} ∣^{2})^{1 / 2}$ on real or complex matrices Spectral network complexity with reference matrices

[F4]

A proper cover has centers in the covered set, and its covering number is the least size of such a finite cover. Proper Frobenius covering numbers

[F5]

The natural logarithm is increasing 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

[F6]

If $A = \sum_{j = 1}^{r} σ_{j} u_{j} v_{j}^{⊤}$ is a singular-value decomposition with $r > 0$ , then $A^{⊤} = \sum_{j = 1}^{r} σ_{j} v_{j} u_{j}^{⊤}$ has the same positive singular values; the largest-singular-value theorem therefore gives equal operator norms. If $r = 0$ , both matrices are zero and their operator norms are zero by the same theorem. Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector

Proof

1.1F1F3F6giveninductionalgebra

Write $Z_{i} (A)$ for the matrix of rowwise layer- $i$ activations, with $Z_{0} (A) = X$ . Induction gives $∥ Z_{i - 1} (A) ∥_{F} \leq ∥ X ∥_{F} \prod_{j < i} ρ_{j} s_{j}$ : rowwise zero-origin Lipschitzness gives $∥ Z_{i} ∥_{F} \leq ρ_{i} ∥ Z_{i - 1} A_{i}^{⊤} ∥_{F}$ , and [F6] identifies $∥ A_{i}^{⊤} ∥_{σ} = ∥ A_{i} ∥_{σ} \leq s_{i}$ , so the induced norm gives $∥ Z_{i - 1} A_{i}^{⊤} ∥_{F} \leq s_{i} ∥ Z_{i - 1} ∥_{F}$ , row by row.

1.2F1givenalgebra

If every $b_{i} = 0$ , each feasible layer set is the singleton ${M_{i}}$ , so $H_{X}$ is a singleton and the right side is zero. Otherwise set $r_{i} = b_{i} / s_{i}$ , $T : = \sum_{i : r_{i} > 0} r_{i}^{2 / 3}$ , and $α_{i} : = r_{i}^{2 / 3} / T$ for positive $r_{i}$ , with $α_{i} = 0$ when $r_{i} = 0$ . These weights are nonnegative and sum to one over the varying layers.

2.1F1F2F4F6step 1.1step 1.2givenconstruct

Build finite proper covers of the attainable layer outputs successively. At layer $i$ , suppose the previous attainable activation matrices have a proper $η$ -cover with centers $V$ that are themselves attainable prefix outputs. For each such $V$ , [F6] gives $∥ A_{i}^{⊤} ∥_{σ} = ∥ A_{i} ∥_{σ}$ , so apply [F2] to ${V A_{i}^{⊤} : A_{i} \in C_{i}}$ with input $V$ , reference $M_{i}^{⊤}$ , radius $e_{i} / ρ_{i}$ , and $e_{i} : = α_{i} ϵ / \prod_{j > i} ρ_{j} s_{j}$ when $b_{i} > 0$ . Map each product-cover center through the rowwise activation $σ_{i}$ . Every resulting center is attainable by joining the prefix that realizes $V$ to its feasible layer matrix. For any actual prefix $Z$ within $η$ of $V$ and any $A_{i} \in C_{i}$ , the activation output differs from $σ_{i} (V A_{i}^{⊤})$ by at most $ρ_{i} s_{i} η$ ; the layer cover adds at most $e_{i}$ . Thus the next-stage cover radius is at most $ρ_{i} s_{i} η + e_{i}$ . When $b_{i} = 0$ , use the single matrix $M_{i}$ and set $e_{i} = 0$ .

3.1F2F4F5step 1.1step 2.1givenalgebra

Starting with the exact cover ${X}$ , the recurrence in step 2.1 gives final radius at most $\sum_{i} e_{i} \prod_{j > i} ρ_{j} s_{j} = ϵ \sum_{i : r_{i} > 0} α_{i} = ϵ$ . The cover is proper by construction. At each varying layer, [F2] and the bound from step 1.1 show that its cover-number logarithm is at most $5 \frac{∥ X ∥_{F}^{2} \prod_{j < i} (ρ_{j} s_{j})^{2} b_{i}^{2}}{(e_{i} / ρ_{i})^{2}} \log (2 d_{i - 1} d_{i}) .$ For each prior cover center $V$ , the next cover has at most this uniform cardinality bound, so taking the union over the prior centers multiplies cardinalities by at most that factor. Since $d_{i - 1}, d_{i} \leq W$ , the logarithm of the final product cover is at most the sum of the displayed layer bounds.

4.1F5step 1.2step 3.1givenalgebra∎

Substitute $e_{i} = α_{i} ϵ / \prod_{j > i} ρ_{j} s_{j}$ into step 3.1. Each varying-layer term becomes $5 \frac{∥ X ∥_{F}^{2}}{ϵ^{2}} \log (2 W^{2}) (\prod_{j = 1}^{L} (ρ_{j} s_{j})^{2}) \frac{r_{i}^{2}}{α_{i}^{2}} .$ By the choice in step 1.2, $\sum_{i : r_{i} > 0} r_{i}^{2} / α_{i}^{2} = T^{3} = (\sum_{i} (b_{i} / s_{i})^{2 / 3})^{3}$ . The all-zero case was handled in step 1.2, so the displayed bound follows in every case.

Source reference

Bartlett, Foster, and Telgarsky, Spectrally-normalized margin bounds for neural networks, Lemma 3.1 and Appendix A.5.

Depends on

Used by

Margin generalization for a bounded spectral-complexity class Lemma

Dependency tree · two levels

29 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.1 and Appendix A.5 (standard reference, not scraped)