The Milman–Pettis theorem

The Milman–Pettis theorem says that every uniformly convex Banach space is reflexive: the canonical map NormedSpace.inclusionInDoubleDual 𝕜 E into the continuous bidual is surjective, over either real or complex scalars. Uniform convexity concerns the underlying real normed space.

Without any completeness assumption, every point φ of the bidual of a uniformly convex space lies within any prescribed ε > 0 of the canonical image of a point of norm at most ‖φ‖, so the canonical image is norm dense in the bidual. For a Banach space this image is also norm closed, because the canonical map is an isometry, and so the canonical map is onto.

Uniform convexity passes to every subspace with the induced norm, so the Milman–Pettis theorem applies to every closed subspace of a uniformly convex Banach space.

Main results

• StrongDual.exists_norm_le_norm_sub_inclusionInDoubleDual_le_of_uniformConvexSpace: the quantitative approximation of a bidual point by the canonical image.
• TauCeti.denseRange_inclusionInDoubleDual_of_uniformConvexSpace: the canonical image of a uniformly convex space is norm dense in its bidual.
• TauCeti.surjective_inclusionInDoubleDual_of_uniformConvexSpace: the Milman–Pettis theorem.
• Submodule.uniformConvexSpace: a subspace of a uniformly convex space is uniformly convex.

Implementation notes

The density statement follows Ringrose's argument from Goldstine's theorem (NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall): on a weak-star open slice where φ is large on a nearly norming functional, uniform convexity confines the canonical image of a ball to a norm ball of radius ε, which is weak-star closed.

References

• R. E. Megginson, An Introduction to Banach Space Theory, Theorem 5.2.15.
• J. R. Ringrose, A note on uniformly convex spaces, J. London Math. Soc. 34 (1959), 92.

instance Submodule.uniformConvexSpace {R : Type u_1} {E : Type u_2} [Ring R] [SeminormedAddCommGroup E] [Module R E] [UniformConvexSpace E] (s : Submodule R E) : UniformConvexSpace ↥s

A subspace of a uniformly convex space, with the induced norm, is uniformly convex.

theorem StrongDual.exists_norm_le_norm_sub_inclusionInDoubleDual_le_of_uniformConvexSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [UniformConvexSpace E] (φ : StrongDual 𝕜 (StrongDual 𝕜 E)) {ε : ℝ} (hε : 0 < ε) : ∃ (x : E), ‖x‖ ≤ ‖φ‖ ∧ ‖φ - (NormedSpace.inclusionInDoubleDual 𝕜 E) x‖ ≤ ε

In a uniformly convex space, every point φ of the bidual lies within any prescribed ε > 0 of the canonical image of a point of norm at most ‖φ‖. No completeness is assumed.

theorem TauCeti.denseRange_inclusionInDoubleDual_of_uniformConvexSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [UniformConvexSpace E] : DenseRange ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)

The canonical image of a uniformly convex space is norm dense in its bidual.

theorem TauCeti.surjective_inclusionInDoubleDual_of_uniformConvexSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [UniformConvexSpace E] [CompleteSpace E] : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)

Milman–Pettis theorem. A uniformly convex Banach space is reflexive: its canonical map into the continuous bidual is surjective.