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.

Exact Lasso coordinate update, including a zero column

Statement

Use the Lasso objective $Q_{y}$ and notation of Lasso estimator for fixed design, with $n, d \geq 1$ and $τ > 0$ . Fix a coordinate $j$ and all other coefficients, and set $r_{j} = y - \sum_{ℓ \neq j} X_{ℓ} θ_{ℓ}$ . If $X_{j} \neq 0$ , the unique minimizing coordinate is $θ_{j}^{+} = \frac{S_{n τ} (X_{j}^{T} r_{j})}{∥ X_{j} ∥_{2}^{2}} .$ If $X_{j} = 0$ , the unique minimizing coordinate is $θ_{j}^{+} = 0$ .

Facts & Assumptions

Given: The fixed-design Lasso objective, a coordinate $j$ , and the other coordinates.

[F1]

Lasso estimator for fixed design: $Q_{y} (θ) = n^{- 1} ∥ y - X θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ , with $τ > 0$ .

[F2]

The one-coordinate absolute-value quadratic minimizer: for $a > 0$ and $λ > 0$ , $\frac{a}{2} u^{2} - b u + λ ∣ u ∣$ has unique minimizer $S_{λ} (b) / a$ .

[F3]

Soft-thresholding map: $S_{λ} (b) = b - λ$ for $b > λ$ , equals $0$ for $∣ b ∣ \leq λ$ , and equals $b + λ$ for $b < - λ$ .

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $∥ v ∥_{2}^{2} = ⟨ v, v ⟩$ and the inner product is bilinear; Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∥ v ∥_{2} = 0$ only for $v = 0$ .

[A1]

The residual excluding coordinate $j$ is $r_{j} = y - \sum_{ℓ \neq j} X_{ℓ} θ_{ℓ}$ .

Proof

1.1F1F4A1algebra

For a candidate value $u$ in coordinate $j$ , $y - X θ = r_{j} - X_{j} u$ . By bilinearity in [F4], expanding the square in [F1] shows that the terms depending on $u$ are $n^{- 1} ∥ X_{j} ∥_{2}^{2} u^{2} - 2 n^{- 1} (X_{j}^{T} r_{j}) u + 2 τ ∣ u ∣$ .

2.1F2F3F4step 1.1algebra

If $X_{j} \neq 0$ , [F4] gives $∥ X_{j} ∥_{2}^{2} > 0$ . Multiply these terms by the positive constant $n / 2$ . The result is $\frac{1}{2} ∥ X_{j} ∥_{2}^{2} u^{2} - (X_{j}^{T} r_{j}) u + n τ ∣ u ∣$ . Apply [F2] with $a = ∥ X_{j} ∥_{2}^{2}$ , $b = X_{j}^{T} r_{j}$ , and $λ = n τ > 0$ to obtain the stated unique minimizer; [F3] fixes its threshold convention at both kink values.

3.1F1A1givenalgebra∎

If $X_{j} = 0$ , the squared-residual term in [F1] is independent of $u$ , while the only varying term is $2 τ ∣ u ∣$ . Since $τ > 0$ , this term has the unique minimum at $u = 0$ .

Depends on

Used by

Dependency tree · two levels

26 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

Stephen J. Wright, Coordinate Descent Algorithms, §2 (standard reference, not scraped)
Clément Royer, Regularized, Large-Scale and Distributed Optimization, Lecture 3, §3.3 (standard reference, not scraped)