Prove2Me

THEOREM (§2), pp. 1–2 — for 0 < δ ≤ 1/4K, S*(x, δ) ≠ ∅ and every sequence with x_{k+1} ∈ S*(x_k, δ) converges to x*

Proved
ArmijoGrad.Conv.convergence_theorem

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

convergencegradient-methodlipschitz-gradientp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1sufficient-decrease

Let f:En→Rf : E^n \to \mathbb{R} be continuous everywhere on EnE^n and bounded below on EnE^n, and fix x0∈Enx_0 \in E^n with level set S(x0)={x:f(x)≤f(x0)}S(x_0) = \{x : f(x) \le f(x_0)\}. Assume:

  1. Condition III at x0x_0: f∈C1f \in C^1 on S(x0)S(x_0) and ∣∇f(y)−∇f(x)∣≤K∣y−x∣|\nabla f(y) - \nabla f(x)| \le K|y - x| for all x,y∈S(x0)x, y \in S(x_0), with K>0K > 0;
  2. Condition IV at x0x_0: f∈C1f \in C^1 on S(x0)S(x_0), x∗x^* satisfies f(x∗)=inf⁡Enff(x^*) = \inf_{E^n} f, and for every r>0r > 0, m(r)=inf⁡{∣∇f(x)∣:x∈S(x0), ∣x−x∗∣≥r}>0m(r) = \inf\{|\nabla f(x)| : x \in S(x_0),\ |x - x^*| \ge r\} > 0 (with m(r)=∞m(r) = \infty if the set is empty).

Let 0<δ≤1/(4K)0 < \delta \le 1/(4K). Then for every x∈S(x0)x \in S(x_0) the set

S∗(x,δ)={xλ:xλ=x−λ∇f(x), λ>0, f(xλ)−f(x)≤−δ∣∇f(x)∣2}S^*(x,\delta) = \{x_\lambda : x_\lambda = x - \lambda\nabla f(x),\ \lambda > 0,\ f(x_\lambda) - f(x) \le -\delta|\nabla f(x)|^2\}

is a nonempty subset of S(x0)S(x_0), and every sequence {xk}k=0∞\{x_k\}_{k=0}^\infty with first term x0x_0 and xk+1∈S∗(xk,δ)x_{k+1} \in S^*(x_k,\delta) for k=0,1,2,…k = 0, 1, 2, \dots converges to x∗x^*.

This is Armijo's convergence theorem for the gradient method: any choice of step that achieves the sufficient decrease δ∣∇f(xk)∣2\delta|\nabla f(x_k)|^2 yields convergence to the minimizer. Both the fixed-step steepest descent method and Armijo's halving rule (Corollaries 1 and 2) are instances.

Formalization Note EnE^n is EuclideanSpace ℝ (Fin n) and ∇f\nabla f is Mathlib's gradient. The paper uses the same symbol x0x_0 for the base point of S(x0)S(x_0) and the first iterate; the formalization makes this explicit with the hypothesis x0=x_0 = first term. Conditions III and IV are assumed on S(x0)S(x_0) only, never on all of EnE^n. Condition IV carries the minimizer x∗x^*; it forces x∗x^* to be the unique minimizer, so the limit is the minimizer of ff.

Preamble
import Mathlib
import Definitions.Def_ArmijoGrad_Conv_Setting

open Filter Topology
Formal statement
namespace ArmijoGrad.Conv

/-- THEOREM (§2), pp. 1–2. If `0 < δ ≤ 1/4K`, then for any `x ∈ S(x₀)` the set `S*(x, δ)` of (1)
is a nonempty subset of `S(x₀)`, and any sequence with `x₀` as first term and
`x_{k+1} ∈ S*(x_k, δ)` converges to the minimizer `x*`. -/
theorem convergence_theorem {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → ℝ) (hf : Continuous f)
    (hbdd : BddBelow (Set.range f)) (x0 : EuclideanSpace ℝ (Fin n)) (K : ℝ)
    (hIII : ConditionIII f x0 K) (xstar : EuclideanSpace ℝ (Fin n))
    (hIV : ConditionIV f x0 xstar) (δ : ℝ) (hδ : 0 < δ) (hδK : δ ≤ 1 / (4 * K)) :
    (∀ x ∈ levelSet f x0, (sdSet f x δ).Nonempty ∧ sdSet f x δ ⊆ levelSet f x0) ∧
      ∀ x : ℕ → EuclideanSpace ℝ (Fin n), x 0 = x0 → (∀ k, x (k + 1) ∈ sdSet f (x k) δ) →
        Tendsto x atTop (𝓝 xstar) := by sorry

end ArmijoGrad.Conv
Source
Armijo, Minimization of functions having Lipschitz continuous first partial derivatives, Pacific J. Math. 16 (1966), pp. 1–2, THEOREM (§2) and (1), under the standing assumptions of §2
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