theorem Chapter3.problem_3_2_lasso_oracle_inequality {n M : ℕ} (hn : 0 < n) (hM : 2 ≤ M) (Φ : Matrix (Fin n) (Fin M) ℝ) (f : Fin n → ℝ) (σ : ℝ) (hσ : 0 < σ) (μ : MeasureTheory.Measure (Fin n → ℝ)) : ∀ {x : MeasureTheory.IsProbabilityMeasure μ} (θhat : (Fin n → ℝ) → Fin M → ℝ) (hLasso : ∀ (ε : Fin n → ℝ), ∃ τ > 0, ∀ (θ : Fin M → ℝ), lassoObjective (f + ε) Φ τ (θhat ε) ≤ lassoObjective (f + ε) Φ τ θ) (hNorm : ∀ (j : Fin M), ∑ i : Fin n, Φ i j ^ 2 ≤ ↑n) (hSubG : ∀ (t : ℝ) (u : Fin n → ℝ), ∫ (ε : Fin n → ℝ), Real.exp (t * ∑ i : Fin n, u i * ε i) ∂μ ≤ Real.exp (σ ^ 2 / 2 * t ^ 2 * ∑ i : Fin n, u i ^ 2)), ∃ (C : ℝ) (c : ℝ), 0 < C ∧ 0 < c ∧ μ {ε : Fin n → ℝ | MSE (Φ.mulVec (θhat ε)) f ≤ ⨅ (θ : Fin M → ℝ), MSE (Φ.mulVec θ) f + C * σ * l1norm θ * √(Real.log ↑M / ↑n)} ≥ ENNReal.ofReal (1 - ↑M ^ (-c))

Problem 3.2 — Exact oracle inequality for the Lasso.

Rigollet, High-Dimensional Statistics, Problem 3.2 (line 2570).

Assume the noise vector ε is sub-Gaussian, ε ~ subGₙ(σ²), and the dictionary columns are normalised so that max_j ‖φⱼ‖₂ ≤ √n. Show that there exists a choice of the tuning parameter τ such that the Lasso estimator θ̂ᴸ with regularisation parameter 2τ satisfies the exact (non-residual) oracle inequality

MSE(φ_{θ̂ᴸ}) ≤ inf_{θ ∈ ℝᴹ} { MSE(φ_θ) + C σ |θ|₁ √(log M / n) }

with probability at least 1 − M⁻ᶜ for positive universal constants C, c.

Unlike the "slow-rate" oracle inequality of Theorem 3.4 (which requires incoherence), this bound holds without any structural assumption on the dictionary beyond column normalisation. The proof uses a direct analysis of the KKT conditions combined with a union-bound argument controlling max_j |⟨φⱼ, ε⟩| via sub-Gaussian maximal inequalities.