LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The proximal map of the l1 norm is soft thresholding

Statement

For $n \geq 1$ and $λ > 0$ , the function $g_{λ} (u) = λ ∥ u ∥_{1}$ is proper, closed and convex in the convention of Proper closed convex extended-real functions on $R^{n}$ . For every $t > 0$ and $v \in R^{n}$ , ${prox}_{t λ ∥ \cdot ∥_{1}} (v) = (S_{t λ} (v_{k}))_{k < n},$ where $S_{τ}$ is the soft-thresholding map of Soft-thresholding map.

Facts & Assumptions

Given: $n \geq 1$ , $λ, t > 0$ , and $v \in R^{n}$ .

[F1]

The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ : $∥ u ∥_{1} = \sum_{k < n} ∣ u_{k} ∣$ and $∥ u - v ∥_{2}^{2} = \sum_{k < n} (u_{k} - v_{k})^{2}$ .

[F2]

Proximal mapping: the proximal point minimizes $λ ∥ u ∥_{1} + ∥ u - v ∥_{2}^{2} / (2 t)$ over $u \in R^{n}$ .

[F3]

Soft-thresholding map: $S_{τ} (s) = s - τ$ if $s > τ$ , $0$ if $∣ s ∣ \leq τ$ , and $s + τ$ if $s < - τ$ .

[F4]

Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page: for $n \geq 1$ , $∥ \cdot ∥_{1}$ is a norm on $R^{n}$ .

[F5]

The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ : for $n \geq 1$ , every norm on $R^{n}$ is continuous in the Euclidean metric.

[F6]

Proper closed convex extended-real functions on $R^{n}$ : properness is nonempty effective domain, convexity is the Jensen inequality, and closedness means closed epigraph.

Proof

1.1F1F4F5F6givenchoosealgebra

Set $h (u) = λ ∥ u ∥_{1}$ . It is finite everywhere and $h (0) = 0$ , so its effective domain is nonempty. By [F4] and $λ > 0$ , the norm triangle and homogeneity inequalities give $h ((1 - θ) u + θ w) \leq (1 - θ) h (u) + θ h (w) (0 \leq θ \leq 1),$ so $h$ is convex. It is continuous by [F5]. To see its epigraph is closed, take any $(u, s)$ with $s < h (u)$ , set $ε = (h (u) - s) / 3$ , and choose $δ_{0} > 0$ so $∥ u^{'} - u ∥_{2} < δ_{0}$ implies $∣ h (u^{'}) - h (u) ∣ < ε$ . If $∥ (u^{'} - u, s^{'} - s) ∥_{2} < \min {δ_{0}, ε}$ in $R^{n + 1}$ , then $s^{'} < s + ε < h (u) - ε < h (u^{'})$ , so this neighborhood misses the epigraph. Thus the complement is open and the epigraph is closed. By [F6], $h$ is proper, closed and convex, as required by the proximal definition.

1.2F3givenalgebra

Fix a scalar $s = v_{k}$ . On $u \geq 0$ , completing the square shows the minimum is at $u = \max {s - t λ, 0}$ ; on $u \leq 0$ it is at $u = \min {s + t λ, 0}$ . If $s > t λ$ , the first candidate is $s - t λ > 0$ and has value strictly below the common boundary value at $0$ , while the second candidate is $0$ . If $s < - t λ$ , the symmetric argument gives the unique minimizer $s + t λ < 0$ . If $- t λ \leq s \leq t λ$ , both half-line minima are $0$ . Thus the unique scalar minimizer is $S_{t λ} (s)$ in all three cases.

2.1F1F2step 1.1givenalgebra

By [F1], the objective in [F2] is the finite sum $\sum_{k < n} ϕ_{k} (u_{k})$ , where $ϕ_{k} (u_{k}) = λ ∣ u_{k} ∣ + (u_{k} - v_{k})^{2} / (2 t)$ . It is enough to find the unique minimizer of each scalar function: the sum is minimized exactly when every coordinate is at its scalar minimum, and the positive quadratic term makes each scalar function strictly convex.

3.1F2step 2.1step 1.2algebra∎

Applying step 1.2 to each of the finitely many coordinates $k < n$ gives the unique vector minimizer $(S_{t λ} (v_{k}))_{k < n}$ , which is the proximal point by [F2].

Depends on

Used by

Dependency tree · two levels

54 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Neal Parikh and Stephen Boyd, Proximal Algorithms, §6.5.2 (standard reference, not scraped)
Amir Beck, First-Order Methods in Optimization, SIAM, 2017, Chapter 6 (standard reference, not scraped)