TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Wide residual networks converge geometrically to zero empirical loss with polynomial depth dependence

Statement

Assume AC, DC and countable choice. Fix positive integers $d, n, H, m$ , training data $x_{1}, \dots, x_{n} \in R^{d}$ and labels $y_{1}, \dots, y_{n} \in R$ with $∥ x_{i} ∥_{2} = 1$ and $∣ y_{i} ∣ \leq C_{y}$ for a fixed finite constant $C_{y}$ . Let the activation satisfy the Lipschitz and smoothness conditions $∣ σ (0) ∣ \leq C_{σ}$ , $∣ σ (z) - σ (z^{'}) ∣ \leq L ∣ z - z^{'} ∣$ , and $∣ σ^{'} (z) - σ^{'} (z^{'}) ∣ \leq β ∣ z - z^{'} ∣$ for finite constants, and also be analytic and nonpolynomial. Use the residual architecture with fixed $0 < c_{r e s} < 1$ and the population matrix $K_{r e s}^{(H)}$ defined on this page, initialized with independent standard normal entries in all weight matrices and the output vector, and trained in all layers by full-batch gradient descent on $L (θ) = \frac{1}{2} \sum_{i = 1}^{n} (f_{r e s} (x_{i}, θ) - y_{i})^{2}$ . Write $K^{(H)} = K_{r e s}^{(H)}$ and put $λ_{0} = λ_{\min} (K^{(H)})$ and assume $λ_{0} > 0$ . For $0 < δ < 1$ , if

$m = Ω ⁣ (\max {\frac{n^{4} H^{6}}{λ_{0}^{4}}, \frac{n^{2}}{λ_{0}^{2} H^{2}}, \frac{n}{δ}, \frac{n^{2} \log (H n / δ)}{λ_{0}^{2}}}), 0 < η = O ⁣ (\frac{λ_{0} H^{2}}{n^{2}}),$

then with probability at least $1 - δ$ over initialization, every gradient-descent iterate $k \geq 1$ satisfies

$L (θ^{(k)}) \leq {(1 - \frac{η λ_{0}}{2})}^{k} L (θ^{(0)}) .$

The constants hidden in $O$ and $Ω$ may depend on the fixed activation, label, and residual-scaling bounds but not on $n, H, m, δ$ ; the step-size constant is small enough that $0 < η λ_{0} / 2 < 1$ . In particular, $L (θ^{(k)}) \to 0$ geometrically as $k \to \infty$ .

Statement references

Du et al., Theorem 6.1 and §3.3

Du et al., Appendix C, Lemmas C.1–C.7 and proof of Theorem 6.1

Facts & Assumptions

Given: The data, architecture, activation, Gaussian initialization, positive terminal population eigenvalue $λ_{0}$ , width, confidence and step-size hypotheses of the Statement.

[F1]

The architecture-specific population kernel, including residual means and scaling, is defined locally and is positive semidefinite. Fully connected and residual networks with the Du Gram kernel The recursively defined population Gram matrices are finite, symmetric, and positive semidefinite

[F2]

The simultaneous Gaussian initialization event gives feature, parameter, backward-coordinate, last-layer Gram, and initial-residual bounds at the stated width. Simultaneous initialization estimates for the Du architectures

[F3]

On parameter balls, the last-layer Gram perturbation and output/loss Hessian have explicit width-dependent bounds. Parameter-ball control of the last-layer Gram and loss Hessian

[F4]

Local Gram positivity and loss-Hessian control confine all GD iterates by a first-exit argument and give geometric loss contraction. Local Gram positivity and loss smoothness give confined gradient descent

[F5]

For square-integrable real random variables, $∣ E X ∣ \leq (E X^{2})^{1 / 2}$ . Cauchy-Schwarz for random variables

Proof

1.1F1F2F3F5givenalgebra

First take $H \geq 2$ and put $λ = λ_{0}$ , $q = 1 + \log (16 / δ)$ . At the stated width, [F2] supplies with probability at least $1 - δ$ a simultaneous event with all constants independent of $H$ , on which $∥ r_{0} ∥^{2} \leq C n q$ and $J_{H} (0) J_{H} (0)^{T} ⪰ 3 λ I / 4$ . By [F1], $S_{i i}^{(1)} = 1$ and $S_{i i}^{(h)} - (b_{i}^{(h)})^{2} \geq 0$ . For $2 \leq h < H$ , put $q_{h} = \sqrt{S_{i i}^{(h)}}$ and $Y_{h} = σ (G_{i}^{(h - 1)})$ . The residual recursion gives $q_{h}^{2} = S_{i i}^{(h - 1)} + 2 α b_{i}^{(h - 1)} E Y_{h} + α^{2} E Y_{h}^{2}$ . By [F1] and [F5], $∣ b_{i}^{(h - 1)} ∣ \leq q_{h - 1}$ and $∣ E Y_{h} ∣ \leq (E Y_{h}^{2})^{1 / 2}$ ; Lipschitz growth and [F5] also give $(E Y_{h}^{2})^{1 / 2} \leq C_{σ} + L q_{h - 1}$ . Hence $q_{h} \leq (1 + α L) q_{h - 1} + α C_{σ}$ . Starting from $q_{1} = 1$ and iterating with $α = c_{r e s} / H$ gives $q_{h} \leq e^{L c_{r e s}} (1 + C_{σ} c_{r e s})$ for every $h < H$ , uniformly in $H$ . The terminal diagonal formula and $∣ σ^{'} ∣ \leq L$ now give $K_{i i}^{(H)} \leq C / H^{2}$ ; positive semidefiniteness in [F1] implies $λ \leq K_{i i}^{(H)} \leq C / H^{2}$ . The residual neighborhood bounds [F3] retain separate first-layer and readout gradients without an erroneous $1 / H$ factor.

2.1F1F3step 1.1algebra

Choose $D = 4 \sqrt{C n q / λ}$ , with $C$ fixed sufficiently large for the initial-residual bound. The width implies $m \geq C n^{3} q / (λ^{3} H^{4})$ and $m \geq C D^{2}$ . To see the logarithmic absorption, use $A_{*} = n^{4} / λ^{4}$ , $B_{*} = n / δ$ and $n^{3} λ^{- 3} \log (1 / δ) \leq (4 / e) \max (A_{*}, B_{*})$ , which follows from $δ^{1 / 4} \log (1 / δ) \leq 4 / e$ exactly as in the fully connected argument. Dividing by $H^{4}$ only decreases the requirement, while the approved width contains $H^{6} A_{*}$ and $B_{*}$ . The constant part is absorbed using $λ H^{2} \leq C$ and $n, H \geq 1$ . Consequently $D / \sqrt{m} \leq c$ and $C n D / (H^{2} \sqrt{m}) \leq λ / 4$ , so the last-layer Gram is at least $λ I / 2$ throughout this ball.

3.1F3step 1.1step 2.1algebra

All constants in the residual Hessian estimate are independent of $H$ . Substitution of $D$ and the initial-residual bound in [F3] yields $∥ \nabla^{2} L ∥ \leq C n + C n^{2} q M / (λ \sqrt{m})$ , because $λ \leq C$ and $n, q \geq 1$ . The approved width and $λ \leq C / H^{2}$ imply $m \geq C \max (n, H^{6}, 1 / δ)$ . Thus $M \leq C \sqrt{\log (e m)}$ , $q \leq C \log (e m)$ and $q M / \sqrt{m} \leq C / H^{2}$ : explicitly, $\log (e m)^{3 / 2} \leq C m^{1 / 6}$ for all $m \geq 1$ , so the ratio is at most $C m^{- 1 / 3} \leq C / H^{2}$ . Also $n \leq C n^{2} / (λ H^{2})$ . Therefore $∥ \nabla^{2} L ∥ \leq S = C n^{2} / (λ H^{2})$ on the ball. The permitted sufficiently small fixed step-size constant makes $η \leq 1 / S$ .

4.1F1F2F3F4step 1.1step 2.1step 3.1algebra∎

Since $D > 2 \sqrt{2} ∥ r_{0} ∥ / \sqrt{λ}$ , [F4] confines every iterate to the ball and gives $L (θ^{(k)}) \leq (1 - η λ / 2)^{k} L (θ^{(0)})$ . The step-size constant can ensure $0 < η λ / 2 < 1$ , because $λ H^{2} \leq C$ . This proves geometric convergence on the probability- $1 - δ$ event. For $H = 1$ the architectures and population kernels coincide; the width is exactly the fully connected depth-one restriction up to fixed constants, and its local proof applies with the same contraction and step-size form. The same application bounds the total parameter path by $2 \sqrt{2} ∥ r_{0} ∥ / \sqrt{λ}$ ; [F3] therefore supplies last-layer Gram stability and the displayed output Taylor-remainder bound on every accepted update segment, for all iterates simultaneously.

Remarks

The displayed sufficient width retains the approved stronger depth restriction. The first term in the official Theorem 6.1 is $n^{4} / (λ_{0}^{4} H^{6})$ , whereas the displayed term is $n^{4} H^{6} / λ_{0}^{4}$ . The proof here establishes the displayed approved restriction by a parameter-ball argument, retaining all trainable layers. It does not claim the sharper source width from this argument. The residual population kernel includes its mean cross terms and differs from the fully connected kernel.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai, Gradient Descent Finds Global Minima of Deep Neural Networks, Theorem 6.1 (standard reference, not scraped)
Simon S. Du, Jason D. Lee, Haochuan Li, Liwei Wang, and Xiyu Zhai, Gradient Descent Finds Global Minima of Deep Neural Networks, Appendix C (standard reference, not scraped)