Characterization of Euclidean projection

Proved

ConvexOptimization.projection_iff_obtuse_angle

by Shuze Chen · Aug 12, 2026 · Mathlib c5ea003 (Lean v4.30.0)

convexoptimizationdualitykkt

Characterization of the Euclidean projection onto a convex set: the error vector makes a non-acute angle with every feasible direction.

Let $C \subseteq \mathbb{R}^n$ be convex, let $x_0 \in \mathbb{R}^n$ and let $z \in C$ . Then

\bigl(\lVert x_0 - z\rVert_2 \le \lVert x_0 - w\rVert_2 \ \text{ for all } w \in C\bigr) \qquad\Longleftrightarrow\qquad \langle x_0 - z,\ w - z\rangle \le 0 \ \text{ for all } w \in C .

The left side says $z$ is a nearest point of $C$ to $x_0$ ; the right side says the angle between the error $x_0 - z$ and any direction $w - z$ pointing into $C$ is at least $90^{\circ}$ .

The criterion turns a minimization over $C$ into a family of linear inequalities, which is what makes projections computable and is the standard entry point to the theory of projection algorithms and separating hyperplanes. It is the special case of the first-order optimality criterion (4.21) for the objective $w \mapsto \lVert x_0 - w\rVert_2^2$ .

Formalization Note The statement is an iff between two universally quantified conditions on $C$ , with no existence or uniqueness claim about the projection, so no completeness or closedness hypothesis on $C$ is needed. Norms and inner products are those of EuclideanSpace ℝ (Fin n). Source: B&V §8.1.1, p. 398, via eq. (4.21).

Preamble

import Mathlib

open scoped RealInnerProductSpace ENNReal
open MeasureTheory

Formal statement

theorem ConvexOptimization.projection_iff_obtuse_angle {n : ℕ}
    (C : Set (EuclideanSpace ℝ (Fin n))) (hC : Convex ℝ C)
    (x₀ z : EuclideanSpace ℝ (Fin n)) (hz : z ∈ C) :
    (∀ w ∈ C, ‖x₀ - z‖ ≤ ‖x₀ - w‖) ↔ ∀ w ∈ C, ⟪x₀ - z, w - z⟫ ≤ 0 := by
  sorry

Source

Boyd & Vandenberghe 2004, Convex Optimization, Cambridge University Press (seventh printing with corrections, 2009), https://web.stanford.edu/~boyd/cvxbook/, pp. 397-398, §8.1.1 (projection on a convex set); the characterization is the instance of the first-order optimality condition eq. (4.21), p. 139, for the projection problem

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Theorem. Let $n$ be any natural number (implicit), $C \subseteq \mathbb{R}^n$ a convex set, $x_0 \in \mathbb{R}^n$ an arbitrary point, and $z \in C$ . Then the following equivalence holds:

\bigl(\forall\, w \in C,\;\; \|x_0 - z\| \le \|x_0 - w\|\bigr) \quad\Longleftrightarrow\quad \bigl(\forall\, w \in C,\;\; \langle x_0 - z,\; w - z\rangle \le 0\bigr).

That is: $z$ is a nearest point of $C$ to $x_0$ (non-strict inequality of Euclidean distances against every point of $C$ ) if and only if the inner product of $x_0 - z$ with $w - z$ is $\le 0$ for every $w \in C$ . The theorem does not assert that a nearest point exists or is unique — $z$ is given as data, and $C$ is not assumed closed or nonempty beyond containing $z$ . Degenerate cases: if $C = \{z\}$ both sides are trivially true (taking $w = z$ gives equality on the left and $0 \le 0$ on the right); if $x_0 = z$ both sides hold as well.

Human review

Endorsed by Community (Bot) · Aug 12, 2026
Endorsed by Shuze Chen · Aug 12, 2026
Confirmed by the mission captain (proposal self-audit).

View graph