TheoremStatement: AI-adaptedProof: 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.

Lasso basic inequality and cone constraint

Statement

Let $Y = X θ^{*} + ε$ be the fixed-design model of Fixed-design regression with sub-Gaussian noise, let $S = {j : θ_{j}^{*} \neq 0}$ , and let $\hat{θ}$ be any minimizer of the objective in Lasso estimator for fixed design with $τ > 0$ . Write $Δ = \hat{θ} - θ^{*}$ . If ${∥ X^{T} ε / n ∥}_{\infty} \leq τ / 2,$ then $\frac{∥ X Δ ∥_{2}^{2}}{n} + τ ∥ Δ_{S^{c}} ∥_{1} \leq 3 τ ∥ Δ_{S} ∥_{1} .$ In particular, $∥ Δ_{S^{c}} ∥_{1} \leq 3 ∥ Δ_{S} ∥_{1}$ , so $Δ \in C (S)$ for the cone in Restricted eigenvalue condition on the Lasso cone.

Facts & Assumptions

Given: A deterministic design $X$ , response $Y = X θ^{*} + ε$ , $τ > 0$ , and a Lasso minimizer $\hat{θ}$ , which exists by The Lasso objective has a nonempty compact convex minimizer set.

[F1]

The Lasso objective is $n^{- 1} ∥ Y - X θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ (Lasso estimator for fixed design).

[F2]

The response has the form $Y = X θ^{*} + ε$ (Fixed-design regression with sub-Gaussian noise).

[F3]

The $ℓ_{1}$ norm is the sum of absolute coordinates (Restricted eigenvalue condition on the Lasso cone).

[F4]

For every response the Lasso minimizer set is nonempty (The Lasso objective has a nonempty compact convex minimizer set).

[F5]

The cone $C (S)$ is defined by $∥ Δ_{S^{c}} ∥_{1} \leq 3 ∥ Δ_{S} ∥_{1}$ (Restricted eigenvalue condition on the Lasso cone).

[A1]

The score bound $∥ X^{T} ε / n ∥_{\infty} \leq τ / 2$ .

Proof

1.1givenF1F2F4algebra

By [F4] choose any minimizer $\hat{θ}$ . Comparison with $θ^{*}$ in [F1] and substitution from [F2] give $\frac{∥ X Δ ∥_{2}^{2}}{n} + 2 τ (∥ \hat{θ} ∥_{1} - ∥ θ^{*} ∥_{1}) \leq \frac{2}{n} ⟨ ε, X Δ ⟩ .$ This follows by expanding $∥ ε - X Δ ∥_{2}^{2}$ and cancelling $∥ ε ∥_{2}^{2}$ .

2.1A1F3F5step 1.1algebra∎

By [A1], writing $g = X^{T} ε / n$ , the finite-coordinate calculation $∣ ⟨ g, Δ ⟩ ∣ \leq \sum_{j} ∣ g_{j} ∣ ∣ Δ_{j} ∣ \leq (\max_{j} ∣ g_{j} ∣) \sum_{j} ∣ Δ_{j} ∣ = ∥ g ∥_{\infty} ∥ Δ ∥_{1}$ bounds the right side of step 1.1 by $τ (∥ Δ_{S} ∥_{1} + ∥ Δ_{S^{c}} ∥_{1})$ . For $j \in S$ , the scalar triangle inequality $∣ θ_{j}^{*} ∣ = ∣ {\hat{θ}}_{j} - Δ_{j} ∣ \leq ∣ {\hat{θ}}_{j} ∣ + ∣ Δ_{j} ∣$ gives $∣ {\hat{θ}}_{j} ∣ - ∣ θ_{j}^{*} ∣ \geq - ∣ Δ_{j} ∣$ ; for $j \notin S$ , $θ_{j}^{*} = 0$ and $∣ {\hat{θ}}_{j} ∣ = ∣ Δ_{j} ∣$ . Summing by [F3] gives $∥ \hat{θ} ∥_{1} - ∥ θ^{*} ∥_{1} \geq - ∥ Δ_{S} ∥_{1} + ∥ Δ_{S^{c}} ∥_{1}$ . Substitution and rearrangement yield the displayed bound. Since $∥ X Δ ∥_{2}^{2} / n \geq 0$ and $τ > 0$ , it implies $∥ Δ_{S^{c}} ∥_{1} \leq 3 ∥ Δ_{S} ∥_{1}$ , which is precisely $Δ \in C (S)$ by [F5].

Depends on

Used by

Lasso prediction and coefficient bounds under incoherence Theorem

Dependency tree · two levels

8 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

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 2, Section 2.4 (standard reference, not scraped)
Peter J. Bickel, Ya'acov Ritov and Alexandre B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Appendix B (standard reference, not scraped)