Convexity of powers of the norm

In every real seminormed space, the q-th power of the norm is a convex function for every exponent 1 ≤ q, as the composition of the convex norm with the convex nondecreasing function t ↦ t ^ q on [0, ∞). In particular, for 0 ≤ a every quadratic x ↦ (a / 2) ‖x‖² + c is convex.

In a strictly convex real normed space, the q-th power of the norm is a strictly convex function for every exponent 1 < q. Both kinds of strictness are needed: strict convexity of t ↦ t ^ q on [0, ∞) separates points of different norms, and strict convexity of the space separates distinct points of equal norm. The exponent q = 1 is excluded, since the norm itself is affine along every ray.

This is the pointwise input for strict convexity of the spaces Lᵖ(μ; E) with 1 < p < ∞ (MeasureTheory.Lp.strictConvexSpace).

Main statements

• TauCeti.convexOn_norm_rpow — x ↦ ‖x‖ ^ q is convex on a real seminormed space, for 1 ≤ q.
• TauCeti.convexOn_mul_norm_sq_add — x ↦ (a / 2) ‖x‖² + c is convex on every convex set, for 0 ≤ a.
• TauCeti.strictConvexOn_norm_rpow — x ↦ ‖x‖ ^ q is strictly convex on a strictly convex real normed space, for 1 < q.

theorem TauCeti.convexOn_norm_rpow {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {q : ℝ} (hq : 1 ≤ q) : ConvexOn ℝ Set.univ fun (x : E) => ‖x‖ ^ q

Convexity of powers of the norm. In a real seminormed space, the function x ↦ ‖x‖ ^ q is convex for every exponent 1 ≤ q.

theorem TauCeti.convexOn_mul_norm_sq_add {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : Convex ℝ s) {a : ℝ} (ha : 0 ≤ a) (c : ℝ) : ConvexOn ℝ s fun (x : E) => a / 2 * ‖x‖ ^ 2 + c

For 0 ≤ a, the quadratic x ↦ (a / 2) ‖x‖² + c is convex on every convex set in a real seminormed space.

theorem TauCeti.strictConvexOn_norm_rpow {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [StrictConvexSpace ℝ E] {q : ℝ} (hq : 1 < q) : StrictConvexOn ℝ Set.univ fun (x : E) => ‖x‖ ^ q

Strict convexity of powers of the norm. In a strictly convex real normed space, the function x ↦ ‖x‖ ^ q is strictly convex for every exponent 1 < q.