Strict convexity of Lᵖ spaces

For 1 < p < ∞ and a strictly convex real normed space E, the space Lᵖ(μ; E) is strictly convex. The proof integrates the pointwise strict convexity of v ↦ ‖v‖ ^ p on E (TauCeti.strictConvexOn_norm_rpow): if ‖f‖ = ‖g‖ = 1 and ‖(f + g) / 2‖ = 1, the integrand (‖f‖ ^ p + ‖g‖ ^ p) / 2 - ‖(f + g) / 2‖ ^ p is nonnegative with integral zero, so it vanishes almost everywhere, which forces f = g almost everywhere.

Both endpoint exponents are genuinely excluded: L¹ and L^∞ of a measure space with two disjoint sets of positive finite measure contain nontrivial segments in their unit spheres.

Strict convexity is what makes geodesics unique in a metric space that embeds isometrically in Lᵖ: the only geodesic segment of a strictly convex normed space is the affine one. This is how the one-dimensional Wasserstein space P_p(ℝ), 1 < p < ∞, is seen to be uniquely geodesic.

Main statements

• MeasureTheory.Lp.strictConvexSpace — Lᵖ(μ; E) is strictly convex for 1 < p < ∞ when E is.

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

Lᵖ is strictly convex. For 1 < p < ∞ and a strictly convex real normed space E, the space Lᵖ(μ; E) is strictly convex.