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 Lasso objective has a nonempty compact convex minimizer set

Statement

Fix integers $n, d \geq 1$ , a deterministic matrix $X \in R^{n \times d}$ , a response $y \in R^{n}$ , and a penalty $τ > 0$ . The minimizer set $M (y)$ of Lasso estimator for fixed design is nonempty, compact, and convex.

Facts & Assumptions

Given: $n, d \geq 1$ , $X \in R^{n \times d}$ , $y \in R^{n}$ , and $τ > 0$ .

[F1]

$Q_{y} (θ) = n^{- 1} ∥ y - X θ ∥_{2}^{2} + 2 τ ∥ θ ∥_{1}$ and $M (y) = \arg \min_{θ} Q_{y} (θ)$ (Lasso estimator for fixed design).

[F2]

Closed bounded subsets of $R^{d}$ are compact, and continuous real functions on nonempty compact sets attain minima (For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent).

[F3]

The Euclidean norm is $∥ θ ∥_{2} = (\sum_{j} θ_{j}^{2})^{1 / 2}$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

Proof

1.1F1F2F3givenalgebrachoose

The function $Q_{y}$ is continuous. For $0 \leq t \leq 1$ , the identity $∥ t a + (1 - t) b ∥_{2}^{2} = t ∥ a ∥_{2}^{2} + (1 - t) ∥ b ∥_{2}^{2} - t (1 - t) ∥ a - b ∥_{2}^{2}$ proves convexity of the squared-residual term, while $∣ t u + (1 - t) v ∣ \leq t ∣ u ∣ + (1 - t) ∣ v ∣$ in each coordinate proves convexity of $∥ \cdot ∥_{1}$ . Since $∥ θ ∥_{1} = \sum_{j} ∣ θ_{j} ∣ \geq ∥ θ ∥_{2}$ (squaring both sides reduces this to nonnegative cross terms $2 ∣ θ_{j} ∣ ∣ θ_{k} ∣$ ), $Q_{y} (θ) \geq 2 τ ∥ θ ∥_{2} \to \infty$ as $∥ θ ∥_{2} \to \infty$ . Choose $R > 0$ with $2 τ R > Q_{y} (0)$ . By [F2], $Q_{y}$ attains a minimum on the closed radius- $R$ ball; every point outside that ball has objective greater than $Q_{y} (0)$ , so a global minimum is attained inside the ball.

2.1F1F2step 1.1algebra∎

The minimizer set is closed as the inverse image $Q_{y}^{- 1} ({\min Q_{y}})$ of a closed singleton under a continuous function, and it is contained in the closed radius- $R$ ball from step 1.1. Hence it is compact by [F2]. If $θ_{1}, θ_{2}$ are minimizers and $0 \leq t \leq 1$ , convexity gives $Q_{y} (t θ_{1} + (1 - t) θ_{2}) \leq t Q_{y} (θ_{1}) + (1 - t) Q_{y} (θ_{2}) = \min Q_{y}$ ; by minimality equality holds, so the minimizer set is convex.

Depends on

Used by

Dependency tree · two levels

14 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, Definition 2.12 (standard reference, not scraped)
Peter J. Bickel, Ya'acov Ritov and Alexandre B. Tsybakov, Simultaneous Analysis of Lasso and Dantzig Selector, Section 7 (standard reference, not scraped)