def norm_penalty {E : Type u} [NormedAddCommGroup E] (lam : ℝ) : E → EReal

The norm penalty x ↦ λ ‖x‖.

@[simp]

theorem norm_penalty_apply {E : Type u} [NormedAddCommGroup E] (lam : ℝ) (x : E) : norm_penalty lam x = ↑(lam * ‖x‖)

Evaluating norm_penalty λ at x gives the value λ ‖x‖.

theorem norm_penalty_eq_nonnegative_linear_penalty_comp_norm {E : Type u} [NormedAddCommGroup E] (lam : ℝ) : norm_penalty lam = nonnegative_linear_penalty lam ∘ norm

The norm penalty is the radial lift of the scalar nonnegative-ray linear penalty.

theorem prox_norm_penalty_eq_singleton_shrinkage {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : ℝ) (hlam : 0 < lam) (x : E) : prox[norm_penalty lam] x = {(1 - lam / max ‖x‖ lam) • x}

Example 6.19: in a real inner product space, for the norm penalty f(x) = λ ‖x‖ with 0 < λ, the proximal mapping at x is the singleton obtained by radial shrinkage: prox[f] x = {(1 - λ / max {‖x‖, λ}) • x}.

@[simp]

theorem mem_prox_norm_penalty_iff {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : ℝ) (hlam : 0 < lam) {x u : E} : u ∈ prox[norm_penalty lam] x ↔ u = (1 - lam / max ‖x‖ lam) • x

A vector belongs to prox[norm_penalty lam] x exactly when it equals the radial shrinkage candidate from Example 6.19.

theorem prox_norm_penalty_eq_singleton_zero_of_norm_le {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : ℝ) (hlam : 0 < lam) (x : E) (hx : ‖x‖ ≤ lam) : prox[norm_penalty lam] x = {0}

If ‖x‖ ≤ λ, then the proximal mapping of x ↦ λ ‖x‖ collapses to the singleton {0}.

theorem prox_norm_penalty_eq_singleton_shrinkage_of_lt_norm {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (lam : ℝ) (hlam : 0 < lam) (x : E) (hx : lam < ‖x‖) : prox[norm_penalty lam] x = {(1 - lam / ‖x‖) • x}

If λ < ‖x‖, then the proximal point is the usual nonzero radial shrinkage (1 - λ / ‖x‖) • x.