Prove2Me

Eq. (2.5) — descent estimate along a run

Proved
CalamaiMore.Convergence.run_descent

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

descentgradient-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 EE, f:E→Rf : E \to \mathbb R continuously differentiable on Ω\Omega, and let (xk,αk)(x_k, \alpha_k) be a run of the gradient projection method (2.1)–(2.3) with constants γ1,γ2>0\gamma_1, \gamma_2 > 0 and μ1,μ2∈(0,1)\mu_1, \mu_2 \in (0,1). Then for every k≥0k \ge 0,

⟨∇f(xk),xk−xk+1⟩≥∥xk+1−xk∥2αk.\langle \nabla f(x_k), x_k - x_{k+1} \rangle \ge \frac{\|x_{k+1} - x_k\|^2}{\alpha_k}.

Combined with the sufficient decrease condition (2.1), this bounds the decrease of ff from below by the squared step length divided by the step.

Preamble
import Mathlib
import Definitions.Def_CalamaiMore_Convergence_IsGradientProjectionRun
Formal statement
namespace CalamaiMore.Convergence

/-- Calamai–Moré, Eq. (2.5) (p. 98): along a run of the gradient projection method,
`⟨∇f(x_k), x_k - x_{k+1}⟩ ≥ ‖x_{k+1} - x_k‖² / α_k` for every `k`. -/
theorem run_descent {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 α)
    (k : ℕ) :
    ‖x (k + 1) - x k‖ ^ 2 / α k ≤ inner ℝ (gradient f (x k)) (x k - x (k + 1)) := by sorry

end CalamaiMore.Convergence
Source
Calamai & Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), p. 98, Eq. (2.5)
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