Prove2Me

Lemma 2.2 — ∥P(x+αd)−x∥/α\|P(x + \alpha d) - x\|/\alpha is nonincreasing

Proved
CalamaiMore.Convergence.step_ratio_antitone

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

gradient-projectionp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1projection

Let Ω\Omega be a nonempty closed convex subset of a finite-dimensional real inner product space EE and PP the projection into Ω\Omega. Given x∈Ex \in E and d∈Ed \in E, the function

ψ(α)=∥P(x+αd)−x∥α,α>0,\psi(\alpha) = \frac{\|P(x + \alpha d) - x\|}{\alpha}, \qquad \alpha > 0,

is antitone (nonincreasing) on (0,∞)(0, \infty).

This result, due to Gafni and Bertsekas, compares the projected steps for two different step sizes along the same direction; it is the key tool for handling steps αk\alpha_k that are not bounded away from zero.

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

/-- Calamai–Moré, Lemma 2.2 (p. 98): for any `x d`, the function
`ψ(α) = ‖P(x + α d) - x‖ / α` is nonincreasing on `α > 0`. -/
theorem step_ratio_antitone {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (Ω : Set E) (hΩne : Ω.Nonempty) (hΩc : IsClosed Ω) (hΩcv : Convex ℝ Ω)
    (x d : E) :
    AntitoneOn (fun a : ℝ => ‖proj Ω (x + a • d) - x‖ / a) (Set.Ioi 0) := by sorry

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