theorem ERealFunction.supportFunction_Icc_neg_one_one_eq_abs : σ[Set.Icc (-1) 1] = Function.asEReal (Function.toEReal fun (ξ : ℝ) => |ξ|)

The support function of the interval [-1,1] ⊆ ℝ is the absolute value.

theorem ERealFunction.subdifferential_abs_eq_piecewise (ξ : ℝ) : subdifferential (Function.toEReal fun (η : ℝ) => |η|) ξ = if ξ < 0 then {-1} else if ξ = 0 then Set.Icc (-1) 1 else {1}

Example 16.15: since |·| = σ[[-1,1]], the subdifferential of the absolute value on ℝ is {-1} on (-∞,0), [-1,1] at 0, and {1} on (0,+∞).