Uniform convexity of Lᵖ spaces for 1 < p < ∞

Let E be a uniformly convex real normed space and 1 < p < ∞. For every η > 0 there is δ > 0 such that

‖f + g‖ ^ p + δ * ‖f - g‖ ^ p ≤ (2 ^ (p - 1) + δ * η) * (‖f‖ ^ p + ‖g‖ ^ p)

for all f g : Lp E p μ. This is the integral of the pointwise inequality TauCeti.exists_forall_norm_add_rpow_add_mul_norm_sub_rpow_le. On the unit sphere, taking η small compared with ‖f - g‖ ^ p bounds ‖f + g‖ away from 2, so the Lebesgue–Bochner space Lp E p μ is uniformly convex. By the Milman–Pettis theorem it is then reflexive when E is complete. The scalar spaces Lp ℝ p μ and Lp ℂ p μ are the main examples, and so is Lp E p μ for a Hilbert space E.

When the norm of E satisfies the parallelogram identity and 2 ≤ p < ∞, integrating the pointwise Clarkson inequality TauCeti.norm_add_rpow_add_norm_sub_rpow_le gives the sharper Clarkson inequality

‖f + g‖ ^ p + ‖f - g‖ ^ p ≤ 2 ^ (p - 1) * (‖f‖ ^ p + ‖g‖ ^ p),

which yields an explicit modulus of convexity.

Main statements

• MeasureTheory.Lp.norm_add_rpow_add_norm_sub_rpow_le: Clarkson's inequality for Lᵖ, 2 ≤ p < ∞.
• MeasureTheory.Lp.exists_forall_norm_add_rpow_add_mul_norm_sub_rpow_le: the uniform convexity estimate for Lᵖ, 1 < p < ∞, with values in a uniformly convex space.
• MeasureTheory.Lp.uniformConvexSpace: Lp E p μ is uniformly convex for 1 < p < ∞.
• MeasureTheory.Lp.surjective_inclusionInDoubleDual: for complete uniformly convex E, Lp E p μ is reflexive for 1 < p < ∞.

References

• J. A. Clarkson, Uniformly convex spaces, Trans. Amer. Math. Soc. 40 (1936), 396–414.
• M. M. Day, Some more uniformly convex spaces, Bull. Amer. Math. Soc. 47 (1941), 504–507.
• H. Brezis, Functional Analysis, Sobolev Spaces and Partial Differential Equations, Theorem 4.10.

theorem MeasureTheory.Lp.norm_add_rpow_add_norm_sub_rpow_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} [InnerProductSpaceable E] (hp : 2 ≤ p) (hp_top : p ≠ ⊤) (f g : ↥(Lp E p μ)) : ‖f + g‖ ^ p.toReal + ‖f - g‖ ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f‖ ^ p.toReal + ‖g‖ ^ p.toReal)

Clarkson's inequality. For 2 ≤ p < ∞ and f g : Lp E p μ, where the norm of E satisfies the parallelogram identity, ‖f + g‖ ^ p + ‖f - g‖ ^ p ≤ 2 ^ (p - 1) * (‖f‖ ^ p + ‖g‖ ^ p).

theorem MeasureTheory.Lp.exists_forall_norm_add_rpow_add_mul_norm_sub_rpow_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} [NormedSpace ℝ E] [UniformConvexSpace E] (hp : 1 < p) (hp_top : p ≠ ⊤) {η : ℝ} (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ ∀ (f g : ↥(Lp E p μ)), ‖f + g‖ ^ p.toReal + δ * ‖f - g‖ ^ p.toReal ≤ (2 ^ (p.toReal - 1) + δ * η) * (‖f‖ ^ p.toReal + ‖g‖ ^ p.toReal)

The uniform convexity estimate for Lᵖ. Let E be a uniformly convex real normed space and 1 < p < ∞. For every η > 0 there is δ > 0 such that for all f g : Lp E p μ, ‖f + g‖ ^ p + δ * ‖f - g‖ ^ p ≤ (2 ^ (p - 1) + δ * η) * (‖f‖ ^ p + ‖g‖ ^ p). The constant δ depends only on E, p and η.

theorem MeasureTheory.Lp.uniformConvexSpace {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} [NormedSpace ℝ E] [UniformConvexSpace E] [Fact (1 ≤ p)] (hp : 1 < p) (hp_top : p ≠ ⊤) : UniformConvexSpace ↥(Lp E p μ)

Lᵖ is uniformly convex for 1 < p < ∞ when E is a uniformly convex real normed space.

theorem MeasureTheory.Lp.surjective_inclusionInDoubleDual {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup E] {p : ENNReal} {𝕜 : Type u_3} [RCLike 𝕜] [Fact (1 ≤ p)] [NormedSpace 𝕜 E] [CompleteSpace E] [UniformConvexSpace E] (hp : 1 < p) (hp_top : p ≠ ⊤) : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 ↥(Lp E p μ))

Lᵖ is reflexive for 1 < p < ∞ when E is a real or complex Banach space that is uniformly convex, such as ℝ, ℂ or a Hilbert space. This is the Milman–Pettis theorem applied to MeasureTheory.Lp.uniformConvexSpace.