Pipeline-generated

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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Linear prediction, shrinkage, and sparse regression — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passOpen item page →

Duplicate predictors give a least-squares line, a ridge point, and a lasso segment

Example

Take $n = 1$ , $p = 2$ , $X = (1 1)$ , and $y = 1$ . The OLS minimizers are exactly ${(β_{1}, β_{2}) : β_{1} + β_{2} = 1}$ . Ridge with parameter $1$ has the unique minimizer $(1 / 3, 1 / 3)$ . Lasso with the empirical-loss convention and penalty $λ = 1 / 4$ has the full minimizer set ${(β_{1}, β_{2}) : β_{1}, β_{2} \geq 0, β_{1} + β_{2} = 3 / 4}$ .

Example references

The Elements of Statistical Learning, §§3.2 and 3.4

Rigollet and Hütter, §2.2

Facts & Assumptions

Given: The fixed design $X = (1 1)$ , response $y = 1$ , the OLS and ridge objectives, and Lasso penalty $λ = 1 / 4$ .

[F1]

OLS minimizers solve the normal equations and ridge has its unique closed-form minimizer (The full ordinary least-squares solution set and the unique ridge solution).

[F2]

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

Verification

1.1F1givenalgebra

Here $X^{T} X = (\begin{array}{cc} 1 & 1 \\ 1 & 1 \end{array})$ and $X^{T} y = (1, 1)^{T}$ . The OLS normal equations reduce to $β_{1} + β_{2} = 1$ , giving the stated full line.

2.1F1step 1.1algebra

For ridge parameter $1$ , $X^{T} X + I_{2} = (\begin{array}{cc} 2 & 1 \\ 1 & 2 \end{array})$ , whose inverse sends $(1, 1)^{T}$ to $(1 / 3, 1 / 3)^{T}$ .

3.1F2givenalgebra∎

Write $t = β_{1} + β_{2}$ . Since $∣ β_{1} ∣ + ∣ β_{2} ∣ \geq ∣ t ∣$ , the Lasso objective is at least $\frac{1}{2} (1 - t)^{2} + \frac{1}{4} ∣ t ∣$ , with equality exactly when the coordinates have the same weak sign. The scalar function decreases up to $t = 3 / 4$ and increases after it: on $t > 0$ its derivative is $t - 3 / 4$ , and on $t < 0$ its derivative is $t - 5 / 4 < 0$ . Thus its unique minimizing sum is $t = 3 / 4 > 0$ , where equality in the triangle inequality requires both coordinates nonnegative. This gives exactly the stated segment of minimizers.

Diagram

The axes are $β_{1}$ and $β_{2}$ . The dashed segment is the first-quadrant portion of the OLS line; the solid segment is the full Lasso minimizer set; the point is the ridge minimizer. The algebraic verification above proves the exact sets and point; the diagram is illustrative.

diagram failed to render:
\begin{tikzpicture}[scale=3]
  \draw[->] (-0.08,0) -- (1.15,0) node[right] {$\beta_1$};
  \draw[->] (0,-0.08) -- (0,1.12) node[above] {$\beta_2$};
  \draw[dashed,gray,thick] (0,1) -- (1,0) node[pos=.22,above right] {OLS};
  \draw[blue,very thick] (0,0.75) -- (0.75,0) node[pos=.25,above right] {Lasso};
  \fill[red] (0.3333,0.3333) circle (0.018) node[above right] {ridge};
  \foreach \x in {0.25,0.5,0.75,1.0} {\draw (\x,0.012) -- (\x,-0.012) node[below=2pt] {\x};}
  \foreach \y in {0.25,0.5,0.75,1.0} {\draw (0.012,\y) -- (-0.012,\y) node[left=2pt] {\y};}
\end{tikzpicture}

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

An orthonormal design makes the Lasso threshold visible coordinate by coordinate

Example

Let $n = p = 2$ , $X = I_{2}$ , $y = (3, - 1)^{T}$ , and use Lasso penalty $λ = 1 / 2$ . Under the empirical loss $∥ y - X β ∥_{2}^{2} / (2 n)$ , the unique Lasso minimizer is $(2, 0)^{T}$ because the threshold is $n λ = 1$ . OLS is $(3, - 1)^{T}$ , and ridge with parameter $1$ is $(3 / 2, - 1 / 2)^{T}$ .

Example references

The Elements of Statistical Learning, §3.4.1

Rigollet and Hütter, §2.3

Facts & Assumptions

Given: $n = p = 2$ , $X = I_{2}$ , $y = (3, - 1)^{T}$ , Lasso penalty $1 / 2$ , and ridge parameter $1$ .

[F1]

On an orthonormal design, the Lasso minimizer is coordinatewise soft-thresholding at $n λ$ (Lasso on an orthonormal design is coordinatewise soft-thresholding).

[F2]

OLS and ridge have the formulas stated in The full ordinary least-squares solution set and the unique ridge solution.

Verification

1.1F2givenalgebra

Since $X^{T} X = I_{2}$ , OLS gives $X^{T} y = (3, - 1)^{T}$ , and the ridge formula with parameter $1$ gives $(I_{2} + I_{2})^{- 1} y = (3 / 2, - 1 / 2)^{T}$ .

2.1F1givenalgebra∎

The Lasso threshold is $n λ = 2 (1 / 2) = 1$ . Applying [F1] gives $S_{1} (3) = 2$ and $S_{1} (- 1) = 0$ , hence $(2, 0)^{T}$ . The equality case $∣ y_{2} ∣ = n λ$ is assigned zero by the stated soft-threshold formula.

ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A coefficient below the orthonormal Lasso threshold is set to zero

Example

For the one-dimensional fixed design $n = p = 1$ , $X = [1]$ , response $y = β^{*} = 1 / 4$ , and Lasso penalty $λ = 1 / 2$ , the true support is ${1}$ but the unique Lasso minimizer is $0$ . This is a deterministic example with no observation noise; it asserts no random-design probability result.

Example references

The Elements of Statistical Learning, §3.4.1

Rigollet and Hütter, §2.3

Facts & Assumptions

Given: $n = p = 1$ , $X = [1]$ , $y = β^{*} = 1 / 4$ , no noise, and $λ = 1 / 2$ .

[F1]

The orthonormal-design Lasso minimizer is soft-thresholding at $n λ$ (Lasso on an orthonormal design is coordinatewise soft-thresholding).

Verification

1.1F1givenalgebra

Here $X^{T} X = 1$ , $n λ = 1 / 2$ , and $∣ X^{T} y ∣ = 1 / 4 < 1 / 2$ . Therefore $S_{1 / 2} (1 / 4) = 0$ by [F1].

2.1step 1.1givenalgebra∎

The true coefficient is nonzero, so its support is ${1}$ , whereas the estimated coefficient is zero and its support is empty. Thus this choice of penalty misses the support when the coefficient is below the threshold.

Linear prediction, shrinkage, and sparse regression — Examples

2 · Logical flowchart

3 · Definitions, theorems and proofs

4 · Examples, counterexamples and false statements

Duplicate predictors give a least-squares line, a ridge point, and a lasso segment

Example

Example references

Facts & Assumptions

Verification

Diagram

An orthonormal design makes the Lasso threshold visible coordinate by coordinate

Example

Example references

Facts & Assumptions

Verification

A coefficient below the orthonormal Lasso threshold is set to zero

Example

Example references

Facts & Assumptions

Verification

Sources