§2, proof of the THEOREM, p. 2 — for x_{k+1} ∈ S*(x_k, δ) and f bounded below, |∇f(x_k)| → 0

Proved

ArmijoGrad.Conv.gradient_norm_tendsto_zero

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

gradient-methodp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1stationarity

Let $f : E^n \to \mathbb{R}$ be bounded below on $E^n$ , let $x_0 \in E^n$ and $\delta > 0$ , and let $\{x_k\}_{k=0}^\infty$ be a sequence with first term $x_0$ such that $x_{k+1} \in S^*(x_k,\delta)$ for $k = 0, 1, 2, \dots$ Then

|\nabla f(x_k)| \to 0 \qquad (k \to \infty).

This is the step of the proof that turns sufficient decrease into stationarity; Condition IV then turns stationarity into convergence of the iterates.

Formalization Note Continuity and Conditions III and IV are not needed and are omitted. $\nabla f$ is Mathlib's gradient, the same gradient used in the definition of $S^*(x,\delta)$ .

Preamble

import Mathlib
import Definitions.Def_ArmijoGrad_Conv_Setting

open Filter Topology

Formal statement

namespace ArmijoGrad.Conv

/-- §2, proof of the THEOREM, p. 2: if `f` is bounded below, `x₀` is the first term and
`x_{k+1} ∈ S*(x_k, δ)` for every `k`, then `|∇f(x_k)| → 0`. -/
theorem gradient_norm_tendsto_zero {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ)
    (hbdd : BddBelow (Set.range f)) (x0 : EuclideanSpace ℝ (Fin n)) (δ : ℝ) (hδ : 0 < δ)
    (x : ℕ → EuclideanSpace ℝ (Fin n)) (hx0 : x 0 = x0)
    (hseq : ∀ k, x (k + 1) ∈ sdSet f (x k) δ) :
    Tendsto (fun k => ‖gradient f (x k)‖) atTop (𝓝 0) := by sorry

end ArmijoGrad.Conv

Source

Armijo, Minimization of functions having Lipschitz continuous first partial derivatives, Pacific J. Math. 16 (1966), p. 2, §2, proof of the THEOREM, second sentence

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph