def hard_thresholding {α : Type u_1} [AddGroup α] [LinearOrder α] (a : α) : α → Set α

Definition 6.4: the hard-thresholding operator with threshold a sends s to {0} when |s| < a, to {s} when a < |s|, and to {0, s} on the threshold |s| = a.

def «term𝓗[_]» : Lean.ParserDescr

Definition 6.4: the hard-thresholding operator with threshold a sends s to {0} when |s| < a, to {s} when a < |s|, and to {0, s} on the threshold |s| = a.

@[simp]

theorem hard_thresholding_apply {α : Type u_1} [AddGroup α] [LinearOrder α] (a s : α) : 𝓗[a] s = if |s| < a then {0} else if a < |s| then {s} else {0, s}

Evaluating the hard-thresholding operator gives its defining three-branch set-valued formula.

theorem hard_thresholding_of_abs_lt {α : Type u_1} [AddGroup α] [LinearOrder α] {a s : α} (h : |s| < a) : 𝓗[a] s = {0}

Hard thresholding returns only 0 below the threshold.

theorem hard_thresholding_of_lt_abs {α : Type u_1} [AddGroup α] [LinearOrder α] {a s : α} (h : a < |s|) : 𝓗[a] s = {s}

Hard thresholding returns only s above the threshold.

theorem hard_thresholding_of_abs_eq {α : Type u_1} [AddGroup α] [LinearOrder α] {a s : α} (h : |s| = a) : 𝓗[a] s = {0, s}

Hard thresholding returns both 0 and s exactly on the threshold.