noncomputable def radial_ball_clip {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : E

Helper for Example 6.62: radial_ball_clip μ x is the radial projection of x onto the closed ball of radius μ.

theorem radial_ball_clip_eq_radial_retraction {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : radial_ball_clip μ x = (↑μ / max ‖x‖ ↑μ) • x

Helper for Example 6.62: the clipping map is the usual radial retraction written with max ‖x‖ μ.

theorem radial_ball_clip_eq_sub_shrinkage {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : radial_ball_clip μ x = x - (1 - ↑μ / max ‖x‖ ↑μ) • x

Helper for Example 6.62: radial clipping is the identity minus the radial shrinkage factor from the norm proximal formula.

theorem norm_linearization_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x y : E) (hx : x ≠ 0) : ‖‖y‖ - ‖x‖ - ((InnerProductSpace.toDualMap ℝ E) ((1 / ‖x‖) • x)) (y - x)‖ ≤ 1 / (2 * ‖x‖) * ‖y - x‖ ^ 2

Helper for Example 6.62: the norm at a nonzero point admits the expected linearization by the radial functional, with a quadratic remainder bound.

theorem hasFDerivAt_norm_of_ne_zero {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) (hx : x ≠ 0) : HasFDerivAt (fun (y : E) => ‖y‖) ((InnerProductSpace.toDualMap ℝ E) ((1 / ‖x‖) • x)) x

Helper for Example 6.62: away from the origin, the norm has Fréchet derivative y ↦ ⟪x / ‖x‖, y⟫.

theorem hasFDerivAt_huber_quadratic_branch {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : HasFDerivAt (fun (y : E) => 1 / (2 * ↑μ) * ‖y‖ ^ 2) ((InnerProductSpace.toDualMap ℝ E) ((1 / ↑μ) • x)) x

Helper for Example 6.62: the quadratic branch of the Huber function has derivative y ↦ ⟪x / μ, y⟫.

theorem huber_boundary_remainder_bound {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x y : E) (hx : ‖x‖ = ↑μ) : ‖H[μ] y - H[μ] x - ((InnerProductSpace.toDualMap ℝ E) ((1 / ↑μ) • x)) (y - x)‖ ≤ 1 / (2 * ↑μ) * ‖y - x‖ ^ 2

Helper for Example 6.62: on the boundary ‖x‖ = μ, the Huber remainder is still controlled by the same quadratic error with linear part y ↦ ⟪x / μ, y⟫.

theorem hasFDerivAt_huber_function_radial_ball_clip {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : HasFDerivAt H[μ] ((InnerProductSpace.toDualMap ℝ E) ((1 / ↑μ) • radial_ball_clip μ x)) x

Helper for Example 6.62: the Huber function has Fréchet derivative y ↦ ⟪radial_ball_clip μ x / μ, y⟫ at every point.

theorem projection_mapping_closedBall_eq_singleton_radial_ball_clip {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : P[Metric.closedBall 0 ↑μ] x = {radial_ball_clip μ x}

Helper for Example 6.62: radial clipping is exactly the singleton projection onto the closed ball of radius μ.

theorem radial_ball_clip_firmly_nonexpansive {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x y : E) : inner ℝ (radial_ball_clip μ x - radial_ball_clip μ y) (x - y) ≥ ‖radial_ball_clip μ x - radial_ball_clip μ y‖ ^ 2

Helper for Example 6.62: the radial clipping map satisfies the firm nonexpansive inequality for closed-ball projections.

theorem radial_ball_clip_nonexpansive {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) : LipschitzWith 1 (radial_ball_clip μ)

Helper for Example 6.62: radial clipping is 1-Lipschitz.

theorem huber_function_is_inv_mu_smooth {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) : is_l_smooth_on H[μ] Set.univ (1 / ↑μ).toNNReal

Example 6.62: for a positive parameter μ, the Huber function H[μ] is globally (1 / μ)-smooth.

theorem hasFDerivAt_huber_function_inv_mu_smul_sub_shrinkage {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : HasFDerivAt H[μ] ((InnerProductSpace.toDualMap ℝ E) ((1 / ↑μ) • (x - (1 - ↑μ / max ‖x‖ ↑μ) • x))) x

The Fréchet derivative of the Huber function at x is the Riesz functional associated to (1 / μ) • (x - u) at the canonical radial shrinkage point u = (1 - μ / max {‖x‖, μ}) • x. This is the completion-free source-facing rendering of the textbook gradient formula ∇ H_μ(x) = (1 / μ) (x - prox_{μ‖·‖}(x)), with the proximal point written using the Chapter 6 owner formula from Example 6.19.

theorem hasFDerivAt_huber_function_piecewise {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (μ : ↑PosReal) (x : E) : HasFDerivAt H[μ] ((InnerProductSpace.toDualMap ℝ E) (if ‖x‖ ≤ ↑μ then (1 / ↑μ) • x else (1 / ‖x‖) • x)) x

The Fréchet derivative of the Huber function is represented by the usual radial piecewise vector field: (1 / μ) • x on the ball ‖x‖ ≤ μ and (1 / ‖x‖) • x outside it, i.e. x / ‖x‖ in the Euclidean notation of the text.