Prove2Me

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

Proved
CalamaiMore.QP.projection_step_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, and let f:E→Rf : E \to \mathbb{R} be continuously differentiable on Ω\Omega. Let xk∈Ωx_k \in \Omega, let αk>0\alpha_k > 0, and let xk+1=P(xk−αk∇f(xk))x_{k+1} = P(x_k - \alpha_k \nabla f(x_k)) be the gradient projection step. Then

⟨∇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}.

The estimate says that the step direction xk+1−xkx_{k+1} - x_k is a descent direction whenever it is nonzero; combined with the sufficient decrease condition (2.1) it shows that a gradient projection step strictly decreases ff unless xk+1=xkx_{k+1} = x_k.

Formalization Note "Continuously differentiable on Ω\Omega" is stated as differentiability at every point of Ω\Omega together with continuity of gradient f on Ω\Omega, the standing assumption of Section 2 of the paper.

Preamble
import Mathlib
import Definitions.Def_CalamaiMore_QP_proj
Formal statement
namespace CalamaiMore.QP

/-- Calamai–Moré, Eq. (2.5) (p. 98): for a nonempty closed convex `Ω`, an iterate `x_k ∈ Ω`, a
step `α_k > 0` and `x_{k+1} = P(x_k - α_k ∇f(x_k))`,
`⟨∇f(x_k), x_k - x_{k+1}⟩ ≥ ‖x_{k+1} - x_k‖² / α_k`. -/
theorem projection_step_descent {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (Ω : Set E) (hΩne : Ω.Nonempty) (hΩc : IsClosed Ω) (hΩcv : Convex ℝ Ω)
    (f : E → ℝ) (hfd : ∀ y ∈ Ω, DifferentiableAt ℝ f y) (hfc : ContinuousOn (gradient f) Ω)
    (xk xnext : E) (hxk : xk ∈ Ω) (αk : ℝ) (hαk : 0 < αk)
    (hstep : xnext = projPath f Ω xk αk) :
    ‖xnext - xk‖ ^ 2 / αk ≤ inner ℝ (gradient f xk) (xk - xnext) := by sorry

end CalamaiMore.QP
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 · Oct 1, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 1, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph