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.

Margin generalization for a bounded spectral-complexity class

Statement

Assume the axiom of choice.

Fix a finite network architecture with $L \geq 1$ , widths $d_{0}, \dots, d_{L} \geq 1$ , output size $K = d_{L} \geq 2$ , activations, and reference matrices as in the spectral-network-complexity definition. Let $s_{i} > 0$ , $b_{i} \geq 0$ , and let $F$ be the nonempty class with layer constraints $∥ A_{i} ∥_{σ} \leq s_{i}$ and $∥ A_{i}^{⊤} - M_{i}^{⊤} ∥_{2, 1} \leq b_{i}$ . Let $S = ((x_{1}, y_{1}), \dots, (x_{n}, y_{n}))$ be an iid sample from any Borel probability measure on $R^{d_{0}} \times {1, \dots, K}$ , let $X$ be its input matrix with rows $x_{i}^{⊤}$ , and fix $n \geq 1$ , $γ > 0$ , and $0 < δ < 1$ . Set $W : = \max_{0 \leq i \leq L} d_{i}$ . With probability at least $1 - δ$ , every $F_{A} \in F$ satisfies $L_{0} (F_{A}) \leq {\hat{L}}_{γ, S} (F_{A}) + \frac{8}{n} + \frac{36 \sqrt{20} ∥ X ∥_{F} \sqrt{\log (2 W^{2})} \log n}{γ n} (\prod_{i = 1}^{L} ρ_{i} s_{i}) {(\sum_{i = 1}^{L} (b_{i} / s_{i})^{2 / 3})}^{3 / 2} + 3 \sqrt{\frac{\log (2 / δ)}{2 n}} .$ All logarithms are natural. The matrix norm on $X$ is the Frobenius norm, and the empirical margin loss uses the threshold convention $m_{F_{A}} (x_{i}, y_{i}) \leq γ$ .

Statement references

Multiclass margins, ramp loss, and empirical margin loss: defines population error, ramp loss, and empirical margin loss.

Spectral network complexity with reference matrices: fixes the architecture and mixed-norm/spectral-norm conventions.

Spectral and reference-matrix covering entropy for network outputs: bounds the proper Frobenius entropy of the sample score matrices.

A truncated covering integral bounds empirical Rademacher complexity: bounds empirical Rademacher complexity by a truncated covering integral.

Uniform margin-risk deviation from empirical Rademacher complexity: converts empirical loss-class complexity to a uniform margin-risk bound.

Facts & Assumptions

Given: The nonempty bounded layer class, iid sample, sample matrix, fixed positive margin, and confidence level in the Statement.

[F1]

For fixed sample inputs, the score matrices form the class covered in the output-entropy lemma, whose logarithmic covering bound has coefficient $5 ∥ X ∥_{F}^{2} \log (2 W^{2}) \prod_{i} (ρ_{i} s_{i})^{2} (\sum_{i} (b_{i} / s_{i})^{2 / 3})^{3}$ . Spectral and reference-matrix covering entropy for network outputs

[F2]

At a fixed example the margin is the true-label score minus the maximum competing score, and the ramp is the stated piecewise-linear function with breakpoints $- γ$ and $0$ . Multiclass margins, ramp loss, and empirical margin loss

[F3]

For any nonempty $[0, 1]$ -valued loss class on the fixed sample and $0 < α \leq \sqrt{n}$ , its one-sided empirical Rademacher complexity is bounded by the truncated proper-covering integral. A truncated covering integral bounds empirical Rademacher complexity

[F4]

Under the axiom of choice, with probability at least $1 - δ$ , the zero-one risk is bounded by the empirical margin loss, twice the loss-class empirical Rademacher complexity, and the stated confidence term. Uniform margin-risk deviation from empirical Rademacher complexity The Axiom of Choice

[F5]

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

[F6]

The natural logarithm is increasing and obeys its product law. The natural logarithm as the inverse of the exponential function Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

Proof

1.1F2F5givenalgebraconstruct

Fix a realized sample and let $U_{X}$ be its set of score matrices. For score matrices $P, Q$ and example $(x_{i}, y_{i})$ , the true-label coordinate changes by at most $∥ P_{i \cdot} - Q_{i \cdot} ∥_{2}$ , and the maximum competing coordinate changes by at most the same amount, so [F2] gives margin change at most twice this row norm. On each linear piece of the ramp the absolute slope is either $0$ or $1 / γ$ ; the pieces meet continuously at $- γ$ and $0$ , so summing the changes over the at most three pieces between any two inputs proves $∣ ℓ_{γ} (a) - ℓ_{γ} (b) ∣ \leq ∣ a - b ∣ / γ$ . Thus the corresponding loss-vector distance is at most $(2 / γ) ∥ P - Q ∥_{F}$ . Mapping the centers of a proper $γ ϵ / 2$ -cover of $U_{X}$ to their loss vectors therefore gives a proper $ϵ$ -cover of the empirical loss-vector class.

2.1F1step 1.1givenalgebra

Apply [F1] at radius $γ ϵ / 2$ and use step 1.1. For every $ϵ > 0$ , $\log N_{F} (L_{γ} ∣ S, ϵ) \leq \frac{20 ∥ X ∥_{F}^{2} \log (2 W^{2})}{γ^{2} ϵ^{2}} (\prod_{i} (ρ_{i} s_{i})^{2}) {(\sum_{i} (b_{i} / s_{i})^{2 / 3})}^{3} = : \frac{K_{γ}}{ϵ^{2}} .$ Here $L_{γ} ∣ S$ is the set of vectors of ramp-loss values on the fixed sample.

3.1F3F6step 2.1givenalgebra

Use the truncated-integral bound [F3] with $α = 1 / n$ , which satisfies $0 < 1 / n \leq \sqrt{n}$ . From step 2.1, $\sqrt{\log N_{F} (L_{γ} ∣ S, ϵ)} \leq \sqrt{K_{γ}} / ϵ$ . Since $\int_{1 / n}^{\sqrt{n}} d ϵ / ϵ = \log (n \sqrt{n}) = \frac{3}{2} \log n$ , it follows that ${\hat{R}}_{S} (L_{γ}) \leq \frac{4}{n \sqrt{n}} + \frac{18 \sqrt{K_{γ}} \log n}{n} .$ When $n = 1$ the integral is zero and the same expression holds.

4.1F4F5step 3.1givenalgebra∎

Apply [F4] and substitute step 3.1. The term twice $4 / (n \sqrt{n})$ is at most $8 / n$ because $n \geq 1$ . Also $\sqrt{K_{γ}} = \sqrt{20} ∥ X ∥_{F} \sqrt{\log (2 W^{2})} γ^{- 1} (\prod_{i} ρ_{i} s_{i}) (\sum_{i} (b_{i} / s_{i})^{2 / 3})^{3 / 2}$ . This yields exactly the stated inequality.

Source reference

Bartlett, Foster, and Telgarsky, Spectrally-normalized margin bounds for neural networks, Theorem 1.1 and Appendix A.6.

Depends on

Used by

A simultaneous spectral margin bound for multiclass networks Theorem

Dependency tree · two levels

48 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, Theorem 1.1 and Appendix A.6 (standard reference, not scraped)