Proposition 2.2 — the simplex projection is a thresholding

Proved

SimplexProj.Condat.simplex_projection_threshold

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

projectionsimplexthresholding

Let $N \ge 1$ , $a > 0$ , $y \in \mathbb{R}^N$ , and let $x = P_\Delta(y)$ be the Euclidean projection of $y$ onto the simplex $\Delta$ of radius $a$ . Then there exists a unique $\tau \in \mathbb{R}$ such that

x_n = \max\{y_n - \tau, 0\} \qquad \text{for all } n = 1, \dots, N.

This is Proposition 2.2 of Condat (Eq. (6)). It reduces computing $P_\Delta(y)$ to finding the single number $\tau$ , which all the algorithms of the paper do; $\tau$ is then characterized by $\sum_{n} \max\{y_n - \tau, 0\} = a$ .

Formalization Note. $x = P_\Delta(y)$ is the predicate IsSimplexProjection a y x. The hypothesis $a > 0$ is needed for uniqueness of $\tau$ .

Preamble

import Mathlib
import Definitions.Def_SimplexProj_Condat_IsSimplexProjection

Formal statement

namespace SimplexProj.Condat

/-- Condat, Proposition 2.2 (p. 2, Eq. (6)): if `x = P_Δ(y)` is the Euclidean projection of `y`
onto the simplex of radius `a`, there is a unique `τ ∈ ℝ` with `x_n = max {y_n - τ, 0}` for all
`n`. Standing assumptions of p. 1: `N ≥ 1`, `a > 0`. -/
theorem simplex_projection_threshold (N : ℕ) (hN : 1 ≤ N) (a : ℝ) (ha : 0 < a)
    (y x : Fin N → ℝ) (hx : IsSimplexProjection a y x) :
    ∃! τ : ℝ, ∀ n, x n = max (y n - τ) 0 := by sorry

end SimplexProj.Condat

Source

Condat, Fast Projection onto the Simplex and the ℓ1 Ball, HAL hal-01056171v2, p. 2, Proposition 2.2, Eq. (6)

Read-back

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

The theorem has these hypotheses:

$N$ is a natural number with $N \ge 1$ .
$a$ is a real number with $a > 0$ .
$y$ and $x$ are vectors in $\mathbb{R}^N$ (real-valued functions on $\{0,\dots,N-1\}$ ).
$x$ is a simplex projection of $y$ with radius $a$ . This means $\sum_n x_n = a$ , every $x_n \ge 0$ , and 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 .

The conclusion is that there is exactly one real number $\tau$ such that

x_n = \max\{\, y_n - \tau,\ 0 \,\} \quad \text{for every index } n .

"Exactly one" means such a $\tau$ exists and any two such reals are equal.

Degenerate cases: $N = 0$ and $a \le 0$ are excluded by the hypotheses. When $N = 1$ , the hypothesis forces $x = (a)$ , and the conclusion says there is exactly one $\tau$ with $a = \max\{y_0 - \tau, 0\}$ . There is no other restriction on $y$ .

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