Prove2Me

§4.4.3, p. 32 — S_κ(a) = (a − κ)₊ − (−a − κ)₊

Proved
BoydADMM.Prox.softThreshold_eq_posPart

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

p2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-bookp2o-v1shrinkagesoft-thresholding

For κ≥0\kappa\ge0 and every a∈Ra\in\mathbb R, the soft thresholding operator

Sκ(a)={a−κa>κ0∣a∣≤κa+κa<−κS_\kappa(a)=\begin{cases}a-\kappa & a>\kappa\\ 0 & |a|\le\kappa\\ a+\kappa & a<-\kappa\end{cases}

satisfies

Sκ(a)=(a−κ)+−(−a−κ)+,S_\kappa(a)=(a-\kappa)_+-(-a-\kappa)_+,

where (t)+=max⁡(t,0)(t)_+=\max(t,0).

This is the "equivalently" form of soft thresholding, written without cases.

Formalization Note The book leaves κ≥0\kappa\ge0 implicit (it uses κ=λ/ρ\kappa=\lambda/\rho with λ,ρ>0\lambda,\rho>0); for κ<0\kappa<0 the identity fails (e.g. κ=−1\kappa=-1, a=0a=0), so the hypothesis is stated.

Preamble
import Mathlib
import Definitions.Def_BoydADMM_Prox_Basic

open Matrix
Formal statement
namespace BoydADMM.Prox

theorem softThreshold_eq_posPart (κ : ℝ) (hκ : 0 ≤ κ) (a : ℝ) :
    softThreshold κ a = max (a - κ) 0 - max (-a - κ) 0 := by sorry

end BoydADMM.Prox
Source
Boyd, Parikh, Chu, Peleato, Eckstein, Distributed Optimization and Statistical Learning via the Alternating Direction Method of Multipliers, Found. Trends Mach. Learn. 3(1) (2011), p. 32, §4.4.3
Human review

  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by mikedeng1 · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph