Uniform convexity of powers of the norm

Let E be a uniformly convex real normed space and 1 < q. The power mean inequality bounds ‖a + b‖ ^ q by 2 ^ (q - 1) * (‖a‖ ^ q + ‖b‖ ^ q) for all vectors a, b. This file shows that the bound improves by a uniform factor once a and b are far apart relative to their size: for every η > 0 there is δ > 0 such that

‖a + b‖ ^ q ≤ (1 - δ) * 2 ^ (q - 1) * (‖a‖ ^ q + ‖b‖ ^ q) whenever η * (‖a‖ ^ q + ‖b‖ ^ q) ≤ ‖a - b‖ ^ q.

When ‖b‖ is much smaller than ‖a‖, the improvement comes from strict convexity of t ↦ t ^ q; when the two norms are comparable, it comes from uniform convexity of E.

Combining the two cases gives an inequality valid for all a and b, with no side condition:

‖a + b‖ ^ q + δ * ‖a - b‖ ^ q ≤ (2 ^ (q - 1) + δ * η) * (‖a‖ ^ q + ‖b‖ ^ q).

For 2 ≤ q in an inner product space, Clarkson's inequality TauCeti.norm_add_rpow_add_norm_sub_rpow_le is the sharper form with δ = 1 and η = 0. Like Clarkson's inequality, the combined form is linear in q-th powers of norms, so it integrates to the same inequality in Lᵖ. This is how uniform convexity passes from E to the Lebesgue–Bochner spaces Lp E p μ for 1 < p < ∞.

Main statements

• TauCeti.exists_forall_norm_add_rpow_le: the improved power mean inequality for vectors that are far apart.
• TauCeti.exists_forall_norm_add_rpow_add_mul_norm_sub_rpow_le: the combined inequality, valid for all pairs of vectors.

References

• M. M. Day, Some more uniformly convex spaces, Bull. Amer. Math. Soc. 47 (1941), 504–507.

theorem TauCeti.exists_forall_norm_add_rpow_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] {q η : ℝ} (hq : 1 < q) (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (a b : E), η * (‖a‖ ^ q + ‖b‖ ^ q) ≤ ‖a - b‖ ^ q → ‖a + b‖ ^ q ≤ (1 - δ) * 2 ^ (q - 1) * (‖a‖ ^ q + ‖b‖ ^ q)

Uniform convexity of the q-th power of the norm. In a uniformly convex real normed space, for 1 < q and η > 0 there is δ > 0 such that ‖a + b‖ ^ q ≤ (1 - δ) * 2 ^ (q - 1) * (‖a‖ ^ q + ‖b‖ ^ q) whenever η * (‖a‖ ^ q + ‖b‖ ^ q) ≤ ‖a - b‖ ^ q. Without the separation hypothesis this holds with δ = 0, by the power mean inequality.

theorem TauCeti.exists_forall_norm_add_rpow_add_mul_norm_sub_rpow_le {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] [UniformConvexSpace E] {q η : ℝ} (hq : 1 < q) (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (a b : E), ‖a + b‖ ^ q + δ * ‖a - b‖ ^ q ≤ (2 ^ (q - 1) + δ * η) * (‖a‖ ^ q + ‖b‖ ^ q)

A Clarkson-type inequality in uniformly convex spaces. In a uniformly convex real normed space, for 1 < q and η > 0 there is δ > 0 such that for all vectors a and b, ‖a + b‖ ^ q + δ * ‖a - b‖ ^ q ≤ (2 ^ (q - 1) + δ * η) * (‖a‖ ^ q + ‖b‖ ^ q).

Being linear in q-th powers of norms, this inequality integrates to the same inequality in Lᵖ and so shows that Lᵖ is uniformly convex.