LemmaStatement: AI-adaptedProof: 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 stated incoherence bound implies the Lasso restricted eigenvalue condition

Statement

Let $n \geq 1$ , $1 \leq s \leq d$ , and let $X \in R^{n \times d}$ satisfy the incoherence condition of Fixed-design incoherence condition. For every $S \subseteq {1, \dots, d}$ with $∣ S ∣ \leq s$ and every $v \in C (S)$ , $\frac{∥ X v ∥_{2}^{2}}{n} \geq \frac{1}{2} ∥ v_{S} ∥_{2}^{2} .$ Consequently the restricted eigenvalue condition of Restricted eigenvalue condition on the Lasso cone holds with $κ^{2} = 1 / 2$ .

Facts & Assumptions

Given: $X \in R^{n \times d}$ , $n \geq 1$ , $1 \leq s \leq d$ , and the incoherence bound $\max_{j, k} ∣ (X^{T} X / n - I)_{j k} ∣ \leq 1 / (14 s)$ .

[F1]

Put $G = X^{T} X / n$ . The incoherence bound is entrywise and equals $1 / (14 s)$ (Fixed-design incoherence condition).

[F2]

$C (S)$ means $∥ v_{S^{c}} ∥_{1} \leq 3 ∥ v_{S} ∥_{1}$ (Restricted eigenvalue condition on the Lasso cone).

[F3]

For a set $S$ of at most $s$ coordinates, $∥ v_{S} ∥_{1}^{2} \leq ∣ S ∣ ∥ v_{S} ∥_{2}^{2} \leq s ∥ v_{S} ∥_{2}^{2}$ (The Cauchy-Schwarz inequality for finite sums).

[F4]

$v^{T} G v = ∥ X v ∥_{2}^{2} / n \geq 0$ for every $v$ , by the definition of $G$ .

Proof

1.1F1F3algebra

Write $v = v_{S} + v_{S^{c}}$ . Since $v_{S}$ and $v_{S^{c}}$ have disjoint supports, [F1] gives $v_{S}^{T} G v_{S} \geq ∥ v_{S} ∥_{2}^{2} - \frac{1}{14 s} ∥ v_{S} ∥_{1}^{2} \geq \frac{13}{14} ∥ v_{S} ∥_{2}^{2},$ where the second inequality uses [F3].

1.2F1F2F3F4algebra

The same disjoint-support fact makes $v_{S}^{T} I v_{S^{c}} = 0$ . Thus $∣ v_{S}^{T} G v_{S^{c}} ∣ \leq \frac{1}{14 s} ∥ v_{S} ∥_{1} ∥ v_{S^{c}} ∥_{1} \leq \frac{3}{14 s} ∥ v_{S} ∥_{1}^{2} \leq \frac{3}{14} ∥ v_{S} ∥_{2}^{2},$ using [F1], [F2] and [F3]. Also $v_{S^{c}}^{T} G v_{S^{c}} \geq 0$ by [F4].

2.1step 1.1step 1.2algebra∎

Expanding $v^{T} G v$ and using steps 1.1–1.2 gives $v^{T} G v \geq (\frac{13}{14} - 2 \frac{3}{14}) ∥ v_{S} ∥_{2}^{2} = \frac{1}{2} ∥ v_{S} ∥_{2}^{2} .$ This is the stated restricted eigenvalue inequality, including $v_{S} = 0$ (then the cone condition forces $v = 0$ , for which both sides are zero).

Depends on

Used by

Lasso prediction and coefficient bounds under incoherence Theorem

Dependency tree · two levels

17 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, 18.S997 High-Dimensional Statistics, Lemma 2.17 (standard reference, not scraped)
Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Lemma 2.17 (standard reference, not scraped)
Peter J. Bickel, Ya'acov Ritov and Alexandre B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Section 3 (standard reference, not scraped)