Theorem 2.3 — $\|x_{k+1} - x_k\|/\alpha_k \to 0$

Proved

CalamaiMore.Convergence.step_ratio_tendsto_zero

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

convergencegradient-projectionp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\Omega$ be a nonempty closed convex subset of a finite-dimensional real inner product space $E$ , let $f : E \to \mathbb R$ be continuously differentiable on $\Omega$ , and let $(x_k, \alpha_k)$ be a run of the gradient projection method defined by (2.1) and (2.2), with constants $\gamma_1, \gamma_2 > 0$ and $\mu_1, \mu_2 \in (0,1)$ . If $f$ is bounded below on $\Omega$ and $\nabla f$ is uniformly continuous on $\Omega$ , then

\lim_{k \to \infty} \frac{\|x_{k+1} - x_k\|}{\alpha_k} = 0.

No boundedness of the iterates $\{x_k\}$ or of the steps $\{\alpha_k\}$ is assumed. The ratio is a lower bound for $\|\nabla_\Omega f(x_k)\|$ , and the theorem is the main step towards the convergence of the projected gradients (Theorem 3.2).

Preamble

import Mathlib
import Definitions.Def_CalamaiMore_Convergence_IsGradientProjectionRun

Formal statement

namespace CalamaiMore.Convergence

/-- Calamai–Moré, Theorem 2.3 (p. 99): if `f` is bounded below on `Ω` and `∇f` is uniformly
continuous on `Ω`, then `‖x_{k+1} - x_k‖ / α_k → 0`. -/
theorem step_ratio_tendsto_zero {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (Ω : Set E) (hΩne : Ω.Nonempty) (hΩc : IsClosed Ω) (hΩcv : Convex ℝ Ω)
    (f : E → ℝ) (hfd : ∀ x ∈ Ω, DifferentiableAt ℝ f x) (hfc : ContinuousOn (gradient f) Ω)
    (γ₁ γ₂ μ₁ μ₂ : ℝ) (hγ₁ : 0 < γ₁) (hγ₂ : 0 < γ₂)
    (hμ₁ : μ₁ ∈ Set.Ioo (0 : ℝ) 1) (hμ₂ : μ₂ ∈ Set.Ioo (0 : ℝ) 1)
    (x : ℕ → E) (α : ℕ → ℝ) (hrun : IsGradientProjectionRun f Ω γ₁ γ₂ μ₁ μ₂ x α)
    (hbdd : BddBelow (f '' Ω)) (huc : UniformContinuousOn (gradient f) Ω) :
    Filter.Tendsto (fun k => ‖x (k + 1) - x k‖ / α k) Filter.atTop (nhds 0) := by sorry

end CalamaiMore.Convergence

Source

Calamai & Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), p. 99, Theorem 2.3

Human review

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

View graph

Theorem 2.3 — ∥xk+1−xk∥/αk→0\|x_{k+1} - x_k\|/\alpha_k \to 0∥xk+1​−xk​∥/αk​→0

Theorem 2.3 — $\|x_{k+1} - x_k\|/\alpha_k \to 0$