theorem convexOn_subsingleton {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [Subsingleton E] [AddCommMonoid β] [PartialOrder β] [SMul 𝕜 E] [Module 𝕜 β] (s : Set E) (f : E → β) : ConvexOn 𝕜 s f

theorem convexOn_rpow_norm {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {p : ℝ} (hp : 1 ≤ p) : ConvexOn ℝ Set.univ fun (x : E) => ‖x‖ ^ p