TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge 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.

Nonconvex SGD stationarity bound for a uniform randomized iterate

Statement

Assume AC. Let $f : R^{d} \to R$ be continuously differentiable with $L$ -Lipschitz gradient for $L > 0$ , and suppose $f (x) \geq f_{\inf}$ for every $x$ , where $f_{\inf} \in R$ is a lower bound. Let $x_{0}$ be deterministic, $Δ = f (x_{0}) - f_{\inf}$ , and run the unconstrained update of Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates with constant $0 < α \leq 1 / L$ . Suppose $E [G_{k} ∣ F_{k}] = \nabla f (x_{k}), Var (G_{k} ∣ F_{k}) \leq σ^{2}$ almost surely for every $k$ . After generating $x_{0}, \dots, x_{N - 1}$ , independently choose $R$ uniformly from ${0, \dots, N - 1}$ on the finite product extension of the trajectory space; equivalently, $E ∥ \nabla f (x_{R}) ∥_{2}^{2} = N^{- 1} \sum_{k < N} E ∥ \nabla f (x_{k}) ∥_{2}^{2}$ . Then $E ∥ \nabla f (x_{R}) ∥_{2}^{2} \leq \frac{2 Δ}{α N} + L α σ^{2} .$ For fixed $Δ, σ$ , the stepsize $α = \min {1 / L, \sqrt{2 Δ / (L σ^{2} N)}}$ gives an $O (N^{- 1 / 2})$ bound when $Δ, σ > 0$ ; zero cases have the stronger bounds specified in the proof. This is an optimization guarantee, not an inferential or central-limit theorem.

Facts & Assumptions

Given: AC; $f, L, f_{\inf}, x_{0}, Δ, N$ and the stochastic update and conditional oracle assumptions in the Statement.

[A1]

The Axiom of Choice: AC supplies the conditional-expectation classes used in the proof.

[F1]

Filtration-adapted stochastic-gradient oracles and Robbins–Monro updates: the update is $x_{k + 1} = x_{k} - α G_{k}$ , and conditional unbiasedness is interpreted coordinatewise almost surely.

[F2]

Descent inequality for a Lipschitz gradient: for an $L$ -Lipschitz gradient, $f (y) \leq f (x) + ⟨ \nabla f (x), y - x ⟩ + (L / 2) ∥ y - x ∥_{2}^{2}$ .

[F3]

Conditional variance and Conditional variance is well-defined and has the second-moment formula: for a square-integrable scalar coordinate, $Var (X ∣ G) = E [X^{2} ∣ G] - (E [X ∣ G])^{2}$ ; summing this identity over the finitely many coordinates gives the vector second-moment identity.

[F4]

Taking out what is known: finite measurable factors may be taken outside conditional expectation once products are integrable.

[F5]

Basic algebra and order properties of conditional expectation: conditional expectation is linear, preserves order, and preserves ordinary expectation.

[F6]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the Euclidean norm square is the sum of squared coordinates.

[F7]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , and the Euclidean norm satisfies the triangle inequality.

[F8]

The principle of mathematical induction: a property true at the first index and inherited by each successor holds at every natural index.

Proof

1.1F1F2F7F8giveninductionalgebra

The oracle definition [F1] requires each $G_{k}$ used in a conditional variance to be square-integrable. Since $x_{0}$ is deterministic and $α$ is finite, the update and [F8] give square-integrable $x_{k}$ at every finite iteration by induction. The Lipschitz condition and triangle inequality in [F7] give $∥ g_{k} ∥_{2} \leq ∥ \nabla f (0) ∥_{2} + L ∥ x_{k} ∥_{2}$ . Applying [F2] at $0, x_{k}$ , then using [F7] and $2 a b \leq a^{2} + b^{2}$ , bounds $∣ f (x_{k}) ∣$ by $C (1 + ∥ x_{k} ∥_{2}^{2})$ for a finite constant $C$ ; thus $f (x_{k})$ is integrable.

2.1A1F1F2F3F4F5F6step 1.1givenalgebra

Put $g_{k} = \nabla f (x_{k})$ . Apply [F2] with $y = x_{k} - α G_{k}$ and condition on $F_{k}$ . By [F1], [F3], [F4], [F5], and [F6], $E [f (x_{k + 1}) ∣ F_{k}] \leq f (x_{k}) - α ∥ g_{k} ∥_{2}^{2} + \frac{L α^{2}}{2} E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] \leq f (x_{k}) - α (1 - L α / 2) ∥ g_{k} ∥_{2}^{2} + \frac{L α^{2} σ^{2}}{2} .$ The last inequality uses $E [∥ G_{k} ∥_{2}^{2} ∣ F_{k}] = ∥ g_{k} ∥_{2}^{2} + Var (G_{k} ∣ F_{k})$ ; all products are integrable by step 1.1.

3.1F5step 2.1givenalgebra

Since $α \leq 1 / L$ , $1 - L α / 2 \geq 1 / 2$ . Take ordinary expectations in step 2.1 and sum for $k = 0, \dots, N - 1$ . The terms $f (x_{k})$ telescope and $E f (x_{N}) \geq f_{\inf}$ , so $\frac{α}{2} \sum_{k = 0}^{N - 1} E ∥ g_{k} ∥_{2}^{2} \leq Δ + \frac{N L α^{2} σ^{2}}{2} .$ Dividing by $α N / 2$ gives $N^{- 1} \sum_{k < N} E ∥ g_{k} ∥_{2}^{2} \leq 2 Δ / (α N) + L α σ^{2}$ .

4.1step 3.1givenalgebra∎

The independent uniform index has $E ∥ \nabla f (x_{R}) ∥_{2}^{2} = N^{- 1} \sum_{k < N} E ∥ g_{k} ∥_{2}^{2}$ , so step 3.1 proves the stated finite- $N$ estimate. If $Δ, σ > 0$ and the square-root choice is at most $1 / L$ , the two terms in the bound are equal and their sum is $2 \sqrt{2 L Δ σ^{2} / N}$ . If the choice is clipped at $1 / L$ , then $σ^{2} N \leq 2 L Δ$ , and the bound is $2 L Δ / N + σ^{2} \leq 4 L Δ / N$ . If $σ = 0 < Δ$ , choose $α = 1 / L$ to get $2 L Δ / N$ ; if $Δ = 0$ , choose $α = 1 / (L (N + 1))$ to get $σ^{2} / (N + 1)$ . Thus every zero case is covered and the asserted asymptotic order follows.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

52 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

Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning, SIAM Review 60(2) (2018), §4.3, Theorem 4.8 (standard reference, not scraped)
Saeed Ghadimi and Guanghui Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming, §2.1, Theorem 2.1 (standard reference, not scraped)