Problem 2.5: Thresholding as penalized ERM

From Rigollet Chapter 2, Problem 2.5. Hard thresholding solves argmin { |y-θ|₂² + 4τ²|θ|₀ } and soft thresholding solves argmin { |y-θ|₂² + 4τ|θ|₁ }.

theorem problem_2_5_hard_threshold_variational {d : ℕ} (y : Fin d → ℝ) (τ : ℝ) (hτ : 0 < τ) (θ : Fin d → ℝ) : ∑ j : Fin d, (y j - hardThreshold τ y j) ^ 2 + 4 * τ ^ 2 * ↑{j : Fin d | hardThreshold τ y j ≠ 0}.card ≤ ∑ j : Fin d, (y j - θ j) ^ 2 + 4 * τ ^ 2 * ↑{j : Fin d | θ j ≠ 0}.card

Problem 2.5 (hard thresholding). The hard thresholding estimator minimizes |y-θ|₂² + 4τ²|θ|₀ over θ ∈ ℝᵈ.

theorem problem_2_5_soft_threshold_variational {d : ℕ} (y : Fin d → ℝ) (τ : ℝ) (hτ : 0 < τ) (θ : Fin d → ℝ) : ∑ j : Fin d, (y j - softThreshold τ y j) ^ 2 + 4 * τ * ∑ j : Fin d, |softThreshold τ y j| ≤ ∑ j : Fin d, (y j - θ j) ^ 2 + 4 * τ * ∑ j : Fin d, |θ j|

Problem 2.5 (soft thresholding). The soft thresholding estimator minimizes |y-θ|₂² + 4τ|θ|₁ over θ ∈ ℝᵈ.