LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 active coordinates of a signed Lasso optimizer satisfy restricted normal equations

Statement

Let $X \in R^{n \times p}$ , $y \in R^{n}$ , $λ > 0$ , and let $S \subseteq {1, \dots, p}$ be nonempty. Assume the active design $X_{S}$ has full column rank. If an optimizer $\hat{β}$ of $∥ y - X β ∥_{2}^{2} / (2 n) + λ ∥ β ∥_{1}$ has support exactly $S$ and sign vector $b = sgn ({\hat{β}}_{S}) \in {- 1, 1}^{∣ S ∣}$ , then ${\hat{β}}_{S} = (X_{S}^{T} X_{S} / n)^{- 1} (X_{S}^{T} y / n - λ b) .$ This is a necessary active-coordinate condition only; it does not assert that the candidate satisfies any inactive-coordinate condition.

Statement references

Wainwright 2006, §2.3, primal-dual witness construction

Rigollet and Hütter, Definition 2.12

Facts & Assumptions

Given: A finite fixed-design Lasso problem, a nonempty active set $S$ , an optimizer supported on $S$ with nonzero active coordinates, and full column rank of $X_{S}$ .

[F1]

The objective uses loss $∥ y - X β ∥_{2}^{2} / (2 n)$ and penalty $λ ∥ β ∥_{1}$ (Fixed-design least-squares, ridge, lasso, group, and fused objectives).

Proof

1.1F1givenalgebra

Fix an active coordinate $j$ . For $∣ h ∣ < ∣ {\hat{β}}_{j} ∣$ , changing that coefficient by $h$ preserves its sign $b_{j}$ , so the restricted objective is differentiable in $h$ and has a local minimum at $h = 0$ . Its positive difference quotients are nonnegative and its negative difference quotients are nonpositive; since the derivative exists, it is zero. Differentiating the squared loss and the fixed-sign penalty in each active coordinate gives $X_{S}^{T} (X_{S} {\hat{β}}_{S} - y) / n + λ b = 0$ .

2.1step 1.1givenalgebra∎

Full column rank makes $X_{S}^{T} X_{S} / n$ invertible. Rearranging step 1.1 and multiplying by this inverse gives the displayed formula. The argument uses only active stationarity and makes no assertion about inactive coordinates.

Depends on

Fixed-design least-squares, ridge, lasso, group, and fused objectives

Used by

The unrestricted Wainwright signed-support threshold claim fails without active-dimension control False statement

Dependency tree · two levels

2 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

Wainwright, Sharp Thresholds for High-Dimensional and Noisy Recovery of Sparsity, 2006, §2.3 (standard reference, not scraped)
Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Definition 2.12 (standard reference, not scraped)