noncomputable def softThresholder {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) : H → H

The soft thresholder at level ρ, as in formula (4.16).

theorem softThresholder_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) (x : H) : softThresholder ρ x = if ρ < ‖x‖ then (1 - ρ / ‖x‖) • x else 0

The soft thresholder acts by radial shrinkage outside the radius-ρ ball and vanishes inside.

noncomputable def hardThresholder {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ α : ℝ) : H → H

The hard thresholder at level ρ and relaxation parameter α, as in formula (4.17).

theorem hardThresholder_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ α : ℝ) (x : H) : hardThresholder ρ α x = if ρ < ‖x‖ then α • x else 0

The hard thresholder scales vectors outside the radius-ρ ball and vanishes inside.

noncomputable def reflectedSoftThresholder {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) : H → H

The operator T₃ from formula (4.18).

theorem reflectedSoftThresholder_apply {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) (x : H) : reflectedSoftThresholder ρ x = if ρ < ‖x‖ then (1 - 2 * ρ / ‖x‖) • x else -x

The operator T₃ reflects vectors in the closed ball and applies the outer radial formula outside it.

theorem reflectedSoftThresholder_eq_reflectedMap_softThresholder {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ : ℝ) (x : H) : reflectedSoftThresholder ρ x = 2 • softThresholder ρ x - x

Helper for Example 4.17: the reflected soft thresholder is the reflector 2T - Id of the soft thresholder.

theorem softThresholder_firmlyNonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (ρ : ℝ) (hρ : 0 < ρ) : FirmlyNonexpansiveOn Set.univ (softThresholder ρ)

Example 4.17 (1): for positive level ρ, the soft thresholder is firmly nonexpansive.

theorem hardThresholder_quasinonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (ρ α : ℝ) (hα0 : 0 < α) (hα1 : α < 1) : QuasinonexpansiveOn Set.univ (hardThresholder ρ α)

Example 4.17 (2): for 0 < α < 1, the hard thresholder is quasinonexpansive.

theorem hardThresholder_not_nonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [Nontrivial H] (ρ α : ℝ) (hρ : 0 < ρ) (hα0 : 0 < α) (hα1 : α < 1) : ¬LipschitzWith 1 (hardThresholder ρ α)

Example 4.17 (3): for 0 < α < 1, the hard thresholder is not nonexpansive.

theorem hardThresholder_not_quasinonexpansive_at_one {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [Nontrivial H] (ρ : ℝ) (hρ : 0 < ρ) : ¬QuasinonexpansiveOn Set.univ (hardThresholder ρ 1)

Example 4.17 (4): at α = 1, the hard thresholder is not quasinonexpansive.

theorem reflectedSoftThresholder_nonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] (ρ : ℝ) (hρ : 0 < ρ) : LipschitzWith 1 (reflectedSoftThresholder ρ)

Example 4.17 (5): for positive level ρ, the operator T₃ is nonexpansive.

theorem reflectedSoftThresholder_not_firmlyNonexpansive {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [Nontrivial H] (ρ : ℝ) (hρ : 0 < ρ) : ¬FirmlyNonexpansiveOn Set.univ (reflectedSoftThresholder ρ)

Example 4.17 (6): for positive level ρ, the operator T₃ is not firmly nonexpansive.