noncomputable def truncated_linear_penalty (μ : ℝ) (α : ENNReal) : ℝ → EReal

The truncated linear penalty x ↦ μ x on [0, α] ∩ ℝ and ∞ outside that interval.

@[simp]

theorem truncated_linear_penalty_apply (μ x : ℝ) (α : ENNReal) : truncated_linear_penalty μ α x = (δ_ {y : ℝ | 0 ≤ y ∧ ↑y ≤ ↑α}) x + ↑(μ * x)

Evaluating the truncated linear penalty gives the affine term plus the indicator of the feasible interval [0, α] ∩ ℝ.

theorem prox_truncated_linear_penalty_eq_singleton (μ : ℝ) (α : ENNReal) (x : ℝ) : prox[truncated_linear_penalty μ α] x = {if α = ⊤ then max (x - μ) 0 else min (max (x - μ) 0) α.toReal}

Example 6.14: for the function f(x) = μ x on [0, α] ∩ ℝ and ∞ outside, where α ∈ [0, ∞], the proximal mapping at x is the singleton consisting of the projection of x - μ onto [0, α] ∩ ℝ.