Pipeline-generated

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.

✓ 1 result · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 1 also cleared it.

Nonconvex gradient descent and stationarity

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Gradient descent has vanishing gradients when the objective is bounded below along its iterates

Statement

Let $n \geq 1$ , let $F : R^{n} \to R$ be continuously Fréchet differentiable, and let $L > 0$ satisfy $∥ \nabla F (x) - \nabla F (y) ∥_{2} \leq L ∥ x - y ∥_{2} (x, y \in R^{n}) .$ Choose $w_{0} \in R^{n}$ , a fixed step $0 < α \leq 1 / L$ , and a real $\underline{F}$ such that the fixed-step gradient-descent sequence $w_{t + 1} = w_{t} - α \nabla F (w_{t})$ satisfies $F (w_{t}) \geq \underline{F}$ for every $t \geq 0$ . Then, for every integer $T \geq 1$ , the following bounds hold:

$\sum_{t = 0}^{T - 1} ∥ \nabla F (w_{t}) ∥_{2}^{2} \leq \frac{2}{α} (F (w_{0}) - \underline{F})$ ;
$\min_{0 \leq t < T} ∥ \nabla F (w_{t}) ∥_{2}^{2} \leq \frac{2 (F (w_{0}) - \underline{F})}{α T}$ .

Moreover, $∥ \nabla F (w_{t}) ∥_{2} \to 0$ as $t \to \infty$ . The lower bound is required only along this sequence; the conclusion is stationarity, not convergence of the iterates or attainment of a local or global minimum.

Statement references

MIT 6.7220/15.084, Lecture 12: Gradient Descent and Descent Lemmas

Ghadimi and Lan, Stochastic First- and Zeroth-Order Methods for Nonconvex Stochastic Programming

Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning

Facts & Assumptions

Given: The $C^{1}$ objective $F$ , its global $L$ -Lipschitz gradient, $L > 0$ , the initial point $w_{0}$ , the fixed step $0 < α \leq 1 / L$ , the recursively defined sequence, and the lower bound $\underline{F}$ along that sequence.

[F1]

Gradient descent: the fixed-step update map is $x \mapsto x - t_{k} \nabla f (x)$ ; at a stationary point its value is $x$ .

[F2]

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder: total differentiability at a point means a linear first-order approximation with a remainder bounded by $ε ∥ h ∥_{2}$ for every $ε > 0$ and all sufficiently small admissible increments; here $C^{1}$ means this derivative exists everywhere and varies continuously.

[F3]

Descent inequality for a Lipschitz gradient: if $f : R^{n} \to R$ is continuously differentiable and its gradient is $L$ -Lipschitz, then $f (y) \leq f (x) + ⟨ \nabla f (x), y - x ⟩ + \frac{L}{2} ∥ y - x ∥_{2}^{2}$ for all $x, y \in R^{n}$ .

[F4]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: for scalar-valued $F$ , $\nabla F (x)$ is the vector of its coordinate partial derivatives.

[F5]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $⟨ u, v ⟩ = \sum_{k < n} u_{k} v_{k}$ and $∥ u ∥_{2}^{2} = ⟨ u, u ⟩$ on $R^{n}$ .

[F6]

Every complete ordered field is Archimedean: in any complete ordered field $K$ , for every $c \in K$ there is a canonical natural number $q \geq 1$ with $c < q \cdot 1_{K}$ .

[F7]

The reals are complete: with its usual order and field structure, the canonical real field $R$ is a complete totally ordered field, hence a complete ordered field to which [F6] applies.

Proof

1.1givenF1F4

Fix $t \geq 0$ and put $g_{t} = \nabla F (w_{t})$ . The coordinate gradient is as in [F4], and [F1] gives $w_{t + 1} = w_{t} - α g_{t}$ .

1.2givenF2F3F5algebra

Apply [F3] at $x = w_{t}$ , $y = w_{t + 1}$ ; the continuously differentiable hypothesis is specified by [F2], and [F5] gives the Euclidean inner-product and norm identity. Thus $F (w_{t + 1}) \leq F (w_{t}) - α ∥ g_{t} ∥_{2}^{2} + \frac{L α^{2}}{2} ∥ g_{t} ∥_{2}^{2} \leq F (w_{t}) - \frac{α}{2} ∥ g_{t} ∥_{2}^{2}$ , because $L α \leq 1$ .

2.1givenstep 1.2algebra

Sum the inequality in step 1.2 for $t = 0, \dots, T - 1$ ; consecutive objective terms cancel, so $\frac{α}{2} \sum_{t = 0}^{T - 1} ∥ \nabla F (w_{t}) ∥_{2}^{2} \leq F (w_{0}) - F (w_{T}) \leq F (w_{0}) - \underline{F}$ . This proves the finite-sum bound for every $T \geq 1$ .

3.1givenF6F7step 2.1assume-hypchoosealgebra

If the gradient norms did not tend to zero, some $ε > 0$ would satisfy $∥ \nabla F (w_{t}) ∥_{2} \geq ε$ at infinitely many indices. The bound $2 (F (w_{0}) - \underline{F}) / (α ε^{2})$ is real; by [F7], $R$ is a complete ordered field, so [F6] supplies a canonical natural $q$ larger than it. The infinite set of such indices contains $q$ distinct indices; take $T$ larger than all of them. Step 2.1 then gives $q ε^{2} \leq 2 (F (w_{0}) - \underline{F}) / α$ , a contradiction. Thus $∥ \nabla F (w_{t}) ∥_{2} \to 0$ ; the finite selection of indices uses no choice axiom.

4.1step 2.1algebra∎

For each $T \geq 1$ , $T \min_{0 \leq t < T} ∥ \nabla F (w_{t}) ∥_{2}^{2} \leq \sum_{t = 0}^{T - 1} ∥ \nabla F (w_{t}) ∥_{2}^{2}$ . Step 2.1 therefore gives the stated finite-horizon minimum-gradient bound.

4 · Examples, counterexamples and false statements

None yet.