Remark 5.17: Tightness of ‖θ‖₂² ≤ ‖θ‖₁²

For k-sparse vectors θ_j = ω_j · (R/k) from the Varshamov-Gilbert construction, the inequality |θ|₂² ≤ |θ|₁² is tight up to a constant factor. Specifically, when k ≤ 2/β, we have |θ_j|₂² = R²/k ≥ (β/2)|θ_j|₁².

noncomputable def Rigollet.Chapter5.sparseVec {d : ℕ} (ω : Fin d → Bool) (R k : ℝ) : Fin d → ℝ

A k-sparse vector with equal nonzero entries R/k, where ω encodes the support.

theorem Rigollet.Chapter5.l1_norm_sparse {d : ℕ} (ω : Fin d → Bool) (R k : ℝ) (hR : 0 ≤ R) (hk : 0 < k) (hcard : ↑{i : Fin d | ω i = true}.card = k) : ∑ i : Fin d, |sparseVec ω R k i| = R

The ℓ₁ norm of a k-sparse vector ω·(R/k) equals R when ω has exactly k true entries.

theorem Rigollet.Chapter5.l2_sq_sparse {d : ℕ} (ω : Fin d → Bool) (R k : ℝ) (hk : 0 < k) (hcard : ↑{i : Fin d | ω i = true}.card = k) : ∑ i : Fin d, sparseVec ω R k i ^ 2 = R ^ 2 / k

The ℓ₂² norm of a k-sparse vector ω·(R/k) equals R²/k.

theorem Rigollet.Chapter5.remark_5_17_core (k β R : ℝ) (hk : 0 < k) (hβ : 0 < β) (hkβ : k ≤ 2 / β) : β / 2 * R ^ 2 ≤ R ^ 2 / k

Core algebraic fact for Remark 5.17: When 0 < k ≤ 2/β, we have β/2 · R² ≤ R²/k, which captures the tightness of the ℓ₁ vs ℓ₂ bound.

theorem Rigollet.Chapter5.remark_5_17 {d : ℕ} (ω : Fin d → Bool) (R k β : ℝ) (hR : 0 ≤ R) (hk : 0 < k) (hβ : 0 < β) (hcard : ↑{i : Fin d | ω i = true}.card = k) (hkβ : k ≤ 2 / β) : β / 2 * (∑ i : Fin d, |sparseVec ω R k i|) ^ 2 ≤ ∑ i : Fin d, sparseVec ω R k i ^ 2

Remark 5.17: For k-sparse vectors θ_j = ω_j · (R/k) with k ≤ 2/β, |θ_j|₂² ≥ (β/2)|θ_j|₁², showing tightness of |θ|₂² ≤ |θ|₁².