theorem HardThresholding.oracle_bound_and_support_recovery {d : ℕ} (θstar ξ : Fin d → ℝ) (τ : ℝ) (hτ : 0 < τ) (hmax : ∀ (j : Fin d), |ξ j| ≤ τ) : ∑ j : Fin d, (hardThreshold τ (θstar + ξ) j - θstar j) ^ 2 ≤ 16 * ↑{j : Fin d | θstar j ≠ 0}.card * τ ^ 2 ∧ ((∀ (j : Fin d), θstar j ≠ 0 → |θstar j| > 3 * τ) → ∀ (j : Fin d), hardThreshold τ (θstar + ξ) j ≠ 0 ↔ θstar j ≠ 0)

Theorem 2.11 (Rigollet). On the event {max_j |ξ_j| ≤ τ}, the hard thresholding estimator θ̂ᴴᴿᴰ = hardThreshold τ (θ* + ξ) satisfies: (i) ‖θ̂ᴴᴿᴰ - θ*‖₂² ≤ 16 · |θ*|₀ · τ² (oracle inequality), and (ii) if min_{j ∈ supp(θ*)} |θ*_j| > 3τ, then supp(θ̂ᴴᴿᴰ) = supp(θ*) (support recovery).