Definition 2.10: Hard Thresholding Estimator

From Rigollet Chapter 2, Definition 2.10.

The hard thresholding estimator with threshold 2τ > 0 has coordinates: θ̂ⱼᴴᴿᴰ = yⱼ · 𝟙(|yⱼ| > 2τ)

That is, θ̂ⱼᴴᴿᴰ = yⱼ if |yⱼ| > 2τ, and 0 if |yⱼ| ≤ 2τ.

noncomputable def hardThreshold {d : ℕ} (τ : ℝ) (y : Fin d → ℝ) : Fin d → ℝ

Definition 2.10 (Rigollet). The hard thresholding estimator with threshold 2τ > 0 has coordinates θ̂ⱼᴴᴿᴰ = yⱼ · 𝟙(|yⱼ| > 2τ), i.e., θ̂ⱼᴴᴿᴰ = yⱼ if |yⱼ| > 2τ and θ̂ⱼᴴᴿᴰ = 0 if |yⱼ| ≤ 2τ.

noncomputable def softThreshold {d : ℕ} (τ : ℝ) (y : Fin d → ℝ) : Fin d → ℝ

Soft thresholding: shrinks yⱼ toward 0 by 2τ. Definition 2.10 from Rigollet: θ̂ⱼˢᵒᶠᵗ = sign(yⱼ)(|yⱼ| - 2τ)₊

Basic properties of hard thresholding

theorem hardThreshold_eq_of_gt {d : ℕ} {τ : ℝ} {y : Fin d → ℝ} {j : Fin d} (h : |y j| > 2 * τ) : hardThreshold τ y j = y j

If |y j| > 2τ then the hard thresholding estimator keeps y j.

theorem hardThreshold_eq_zero_of_le {d : ℕ} {τ : ℝ} {y : Fin d → ℝ} {j : Fin d} (h : |y j| ≤ 2 * τ) : hardThreshold τ y j = 0

If |y j| ≤ 2τ then the hard thresholding estimator sets the coordinate to 0.

Basic properties of soft thresholding

theorem softThreshold_eq_of_gt {d : ℕ} {τ : ℝ} {y : Fin d → ℝ} {j : Fin d} (h : y j > 2 * τ) : softThreshold τ y j = y j - 2 * τ

If y j > 2τ then the soft thresholding estimator shrinks y j by 2τ.

theorem softThreshold_eq_of_lt_neg {d : ℕ} {τ : ℝ} {y : Fin d → ℝ} {j : Fin d} (hτ : 0 ≤ τ) (h : y j < -(2 * τ)) : softThreshold τ y j = y j + 2 * τ

If y j < -(2τ) (and τ ≥ 0) then the soft thresholding estimator shifts y j by +2τ.

theorem softThreshold_eq_zero_of_abs_le {d : ℕ} {τ : ℝ} {y : Fin d → ℝ} {j : Fin d} (h : |y j| ≤ 2 * τ) : softThreshold τ y j = 0

If |y j| ≤ 2τ then the soft thresholding estimator sets the coordinate to 0.