The projections onto the simplex and the $\ell_1$ ball exist and are unique

Proved

SimplexProj.Condat.projections_exist_unique

by mikedeng1 · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

l1-ballprojectionsimplex

Let $N \ge 1$ , $a > 0$ , and $y \in \mathbb{R}^N$ . Let $\Delta$ be the simplex of radius $a$ and $B$ the $\ell_1$ ball of radius $a$ . Then $y$ has exactly one Euclidean projection onto $\Delta$ and exactly one Euclidean projection onto $B$ :

\exists!\, x \in \mathbb{R}^N,\ x = P_\Delta(y) \qquad\text{and}\qquad \exists!\, x \in \mathbb{R}^N,\ x = P_B(y).

Condat states this in the introduction ("These two projections are well defined and unique, since $\Delta$ and $B$ are closed and convex sets"); it makes $P_\Delta$ and $P_B$ functions, which every later statement of the paper uses.

Formalization Note. " $x = P_\Delta(y)$ " is the predicate IsSimplexProjection a y x, and similarly for $B$ . The hypotheses $N \ge 1$ and $a > 0$ are the paper's standing assumptions (Sect. 1).

Preamble

import Mathlib
import Definitions.Def_SimplexProj_Condat_IsSimplexProjection
import Definitions.Def_SimplexProj_Condat_IsL1Projection

Formal statement

namespace SimplexProj.Condat

/-- Condat, Sect. 1, p. 2: the Euclidean projections `P_Δ(y)` and `P_B(y)` onto the simplex and
the `ℓ1` ball of radius `a` are well defined and unique. Standing assumptions of p. 1:
`N ≥ 1`, `a > 0`. -/
theorem projections_exist_unique (N : ℕ) (hN : 1 ≤ N) (a : ℝ) (ha : 0 < a) (y : Fin N → ℝ) :
    (∃! x : Fin N → ℝ, IsSimplexProjection a y x) ∧ (∃! x : Fin N → ℝ, IsL1Projection a y x) := by sorry

end SimplexProj.Condat

Source

Condat, Fast Projection onto the Simplex and the ℓ1 Ball, HAL hal-01056171v2, p. 2, Sect. 1

Read-back

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

Let $N$ be a natural number with $N \ge 1$ , let $a$ be a real number with $a > 0$ , and let $y \in \mathbb{R}^N$ be any vector (a real-valued function on $\{0,\dots,N-1\}$ ). The theorem asserts two things.

Exactly one simplex projection. There is exactly one $x \in \mathbb{R}^N$ $x \in R^{N}$ with both of these properties:
- $\sum_n x_n = a$ and $x_n \ge 0$ for all $n$ ;
- for every $z$ with $\sum_n z_n = a$ and all $z_n \ge 0$ ,

\sum_n (x_n - y_n)^2 \le \sum_n (z_n - y_n)^2 .

Exactly one $\ell_1$ -ball projection. There is exactly one $x \in \mathbb{R}^N$ $x \in R^{N}$ with both of these properties:
- $\sum_n |x_n| \le a$ ;
- for every $z$ with $\sum_n |z_n| \le a$ ,

\sum_n (x_n - y_n)^2 \le \sum_n (z_n - y_n)^2 .

"Exactly one" means the vector exists and any two such vectors are equal.

Degenerate cases: the hypotheses rule out $N = 0$ and $a \le 0$ , so both constraint sets are nonempty. When $N = 1$ , the first set is the single point $(a)$ , so the first claim says that point is the unique minimizer. The second set is the interval $[-a, a]$ . The statement covers every real vector $y$ , with no further restriction.

Human review

Endorsed by Shuze Chen · Oct 21, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 21, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The projections onto the simplex and the ℓ1\ell_1ℓ1​ ball exist and are unique

The projections onto the simplex and the $\ell_1$ ball exist and are unique