Sect. 2 (p. 5) — $\tau$ is the root of $f(\rho)=\sum_n \max\{y_n-\rho,0\}-a$ ; sign test and bracket

Proved

SimplexProj.Condat.threshold_root_bracket

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

projectionroot-findingsimplex

Let $N \ge 1$ , $a > 0$ , $y \in \mathbb{R}^N$ , let $x = P_\Delta(y)$ be the Euclidean projection of $y$ onto the simplex of radius $a$ , and let $\tau$ be the threshold of Proposition 2.2, so $x_n = \max\{y_n - \tau, 0\}$ for all $n$ . Let $y_{\max}$ and $y_{\min}$ be the largest and smallest entries of $y$ and define

f(\rho) := \sum_{n=1}^N \max\{y_n - \rho, 0\} - a \qquad (\rho \in \mathbb{R}).

Then: $f(\tau) = 0$ ; $f$ is convex; $f$ is piecewise linear with breakpoints at the $y_n$ (it is affine on every closed interval $[\rho_1, \rho_2]$ whose interior contains no $y_n$ ); $f$ is strictly decreasing on $(-\infty, y_{\max}]$ and $f(\rho) = -a$ for every $\rho \ge y_{\max}$ ; for every $\rho$ , $f(\rho) < 0$ implies $\rho > \tau$ and $f(\rho) > 0$ implies $\rho < \tau$ ; $f(y_{\min} - a/N) \ge 0$ , $f(y_{\max} - a/N) \le 0$ and $f(y_{\max} - a) \ge 0$ ; and consequently

\max\{y_{\max} - a,\ y_{\min} - a/N\} \le \tau \le y_{\max} - a/N.

These are the properties Condat lists in Sect. 2 when viewing the search for $\tau$ as root finding; the sign test is what lets an algorithm discard entries on one side of a trial value $\rho$ .

Formalization Note. $f$ , $y_{\max}$ and $y_{\min}$ are given as variables pinned by the hypotheses hf, IsGreatest (Set.range y) ymax and IsLeast (Set.range y) ymin. "Piecewise linear with breakpoints at the $y_n$ " is rendered as: $f$ is affine on every interval $[\rho_1, \rho_2]$ with no $y_n$ in $(\rho_1, \rho_2)$ .

Preamble

import Mathlib
import Definitions.Def_SimplexProj_Condat_IsSimplexProjection

Formal statement

namespace SimplexProj.Condat

/-- Condat, Sect. 2, p. 5: with `f ρ = ∑ₙ max {y_n - ρ, 0} - a` and `τ` the threshold of
Proposition 2.2 (`x = P_Δ(y)`, `x_n = max {y_n - τ, 0}`): `τ` is a root of `f`; `f` is convex,
piecewise linear with breakpoints at the `y_n` (affine on every closed interval whose interior
contains no `y_n`), strictly decreasing on `(-∞, y_max]` and equal to `-a` on `[y_max, +∞)`;
`f ρ < 0 → ρ > τ` and `f ρ > 0 → ρ < τ`; `f (y_min - a/N) ≥ 0`, `f (y_max - a/N) ≤ 0`,
`f (y_max - a) ≥ 0`; hence `τ ∈ [max {y_max - a, y_min - a/N}, y_max - a/N]`.
Standing assumptions of p. 1: `N ≥ 1`, `a > 0`. -/
theorem threshold_root_bracket (N : ℕ) (hN : 1 ≤ N) (a : ℝ) (ha : 0 < a)
    (y x : Fin N → ℝ) (hx : IsSimplexProjection a y x)
    (τ : ℝ) (hτ : ∀ n, x n = max (y n - τ) 0)
    (f : ℝ → ℝ) (hf : ∀ ρ, f ρ = ∑ n, max (y n - ρ) 0 - a)
    (ymax ymin : ℝ) (hmax : IsGreatest (Set.range y) ymax) (hmin : IsLeast (Set.range y) ymin) :
    f τ = 0 ∧
    ConvexOn ℝ Set.univ f ∧
    (∀ ρ₁ ρ₂ : ℝ, ρ₁ ≤ ρ₂ → (∀ n, y n ∉ Set.Ioo ρ₁ ρ₂) →
      ∃ c d : ℝ, ∀ ρ ∈ Set.Icc ρ₁ ρ₂, f ρ = c * ρ + d) ∧
    StrictAntiOn f (Set.Iic ymax) ∧
    (∀ ρ ∈ Set.Ici ymax, f ρ = -a) ∧
    (∀ ρ : ℝ, f ρ < 0 → τ < ρ) ∧
    (∀ ρ : ℝ, 0 < f ρ → ρ < τ) ∧
    0 ≤ f (ymin - a / N) ∧ f (ymax - a / N) ≤ 0 ∧ 0 ≤ f (ymax - a) ∧
    max (ymax - a) (ymin - a / N) ≤ τ ∧ τ ≤ ymax - a / N := by sorry

end SimplexProj.Condat

Source

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

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 $\sum_n (x_n - y_n)^2 \le \sum_n (z_n - y_n)^2$ for every $z$ with $\sum_n z_n = a$ and all $z_n \ge 0$ .
$\tau$ is a real number with $x_n = \max\{y_n - \tau, 0\}$ for every $n$ .
$f : \mathbb{R} \to \mathbb{R}$ is a function satisfying, for every real $\rho$ ,

f(\rho) = \Big(\sum_{n} \max\{y_n - \rho,\ 0\}\Big) - a .

$y_{\max}$ is the greatest value among the entries of $y$ : it equals some $y_n$ , and every $y_n \le y_{\max}$ .
$y_{\min}$ is the least value among the entries of $y$ : it equals some $y_n$ , and every $y_n \ge y_{\min}$ .

In the conclusion, $a/N$ divides by $N$ viewed as a real number. The theorem concludes all twelve of the following:

$f(\tau) = 0$ .
$f$ is convex on all of $\mathbb{R}$ .
For all reals $\rho_1 \le \rho_2$ such that no entry $y_n$ lies in the open interval $(\rho_1, \rho_2)$ , there are reals $c, d$ with $f(\rho) = c\rho + d$ for every $\rho \in [\rho_1, \rho_2]$ .
$f$ is strictly decreasing on $(-\infty, y_{\max}]$ : if $\rho < \rho' \le y_{\max}$ , then $f(\rho) > f(\rho')$ .
$f(\rho) = -a$ for every $\rho \ge y_{\max}$ .
For every real $\rho$ : if $f(\rho) < 0$ , then $\tau < \rho$ .
For every real $\rho$ : if $f(\rho) > 0$ , then $\rho < \tau$ .
$f(y_{\min} - a/N) \ge 0$ .
$f(y_{\max} - a/N) \le 0$ .
$f(y_{\max} - a) \ge 0$ .
$\max\{y_{\max} - a,\ y_{\min} - a/N\} \le \tau$ .
$\tau \le y_{\max} - a/N$ .

Degenerate cases:

$N \ge 1$ , so $a/N$ never divides by zero, and $y_{\max}$ and $y_{\min}$ are entries of $y$ .
In item 3, the case $\rho_1 = \rho_2$ is allowed; there the interval is a single point and the claim is immediate.
When $N = 1$ , $y_{\max} = y_{\min} = y_0$ , and $a/N = a$ , so the bounds in items 11–12 read $y_0 - a \le \tau \le y_0 - a$ .

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

Sect. 2 (p. 5) — τ\tauτ is the root of f(ρ)=∑nmax⁡{yn−ρ,0}−af(\rho)=\sum_n \max\{y_n-\rho,0\}-af(ρ)=∑n​max{yn​−ρ,0}−a; sign test and bracket

Sect. 2 (p. 5) — $\tau$ is the root of $f(\rho)=\sum_n \max\{y_n-\rho,0\}-a$ ; sign test and bracket