theorem uniformConvexOn_norm_sq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : UniformConvexOn Set.univ (fun (r : ℝ) => r ^ 2) fun (x : H) => ‖x‖ ^ 2

Helper for Example 8.10: the squared norm is uniformly convex on the whole space with modulus r ↦ r ^ 2.

theorem strictConvexOn_norm_sq {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℝ H] : StrictConvexOn ℝ Set.univ fun (x : H) => ‖x‖ ^ 2

Example 8.10: the squared norm function x ↦ ‖x‖ ^ 2 is strictly convex on the whole space of a real inner product space.