Lemma 2.1(a) — variational inequality of the projection

Proved

CalamaiMore.QP.proj_variational

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

convex-setp2o-batch-p200ap2o-gran-per-chapterp2o-plan-paperp2o-v1projectionvariational-inequality

Let $\Omega$ be a nonempty closed convex subset of a finite-dimensional real inner product space $E$ and let $P$ be the projection into $\Omega$ . If $z \in \Omega$ , then

\langle P(x) - x,\ z - P(x) \rangle \ge 0 \qquad \text{for all } x \in E.

Geometrically, the vector from $x$ to its projection makes a non-obtuse angle with every direction from $P(x)$ into $\Omega$ . This inequality is the source of the descent estimates (2.4)–(2.5) of the gradient projection method, and it characterises the fixed points of $x \mapsto P(x - \alpha\nabla f(x))$ as the stationary points.

Preamble

import Mathlib
import Definitions.Def_CalamaiMore_QP_proj

Formal statement

namespace CalamaiMore.QP

/-- Calamai–Moré, Lemma 2.1(a) (p. 98): for a nonempty closed convex `Ω`, if `z ∈ Ω` then
`⟨P(x) - x, z - P(x)⟩ ≥ 0` for all `x`. -/
theorem proj_variational {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
    (Ω : Set E) (hΩne : Ω.Nonempty) (hΩc : IsClosed Ω) (hΩcv : Convex ℝ Ω)
    (z : E) (hz : z ∈ Ω) (x : E) :
    0 ≤ inner ℝ (proj Ω x - x) (z - proj Ω x) := by sorry

end CalamaiMore.QP

Source

Calamai & Moré, Projected gradient methods for linearly constrained problems, Math. Programming 39 (1987), p. 98, Lemma 2.1(a)

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