Goldstine's theorem

Goldstine's theorem says that the canonical embedding of a normed space E into its bidual maps the closed unit ball of E onto a weak-star dense subset of the closed unit ball of the bidual. We prove it for every closed ball: the weak-star closure of the image of closedBall x r under NormedSpace.inclusionInDoubleDualWeak is the closed ball of radius r about the image of x. In particular E is weak-star dense in its bidual.

No completeness or separability is assumed, and seminormed spaces are allowed. Together with Banach–Alaoglu (WeakDual.isCompact_closedBall), Goldstine's theorem relates weak compactness of the unit ball of E to reflexivity of E.

Main results

• NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall: Goldstine's theorem.
• NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall_zero_one: its unit-ball form.
• NormedSpace.denseRange_inclusionInDoubleDualWeak: E is weak-star dense in its bidual.

References

• R. E. Megginson, An Introduction to Banach Space Theory, Theorem 2.6.26.

theorem NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (r : ℝ) : closure (⇑(inclusionInDoubleDualWeak 𝕜 E) '' ⇑(toWeakSpace 𝕜 E) '' Metric.closedBall x r) = ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall ((inclusionInDoubleDual 𝕜 E) x) r

Goldstine's theorem. The weak-star closure of the image of the closed ball closedBall x r under the canonical embedding into the bidual is the closed ball of radius r about the image of x.

theorem NormedSpace.closure_image_inclusionInDoubleDualWeak_closedBall_zero_one (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : closure (⇑(inclusionInDoubleDualWeak 𝕜 E) '' ⇑(toWeakSpace 𝕜 E) '' Metric.closedBall 0 1) = ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1

Goldstine's theorem, unit-ball form: the closed unit ball of E has weak-star dense image in the closed unit ball of its bidual.

theorem NormedSpace.denseRange_inclusionInDoubleDualWeak (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : DenseRange ⇑(inclusionInDoubleDualWeak 𝕜 E)

A normed space is weak-star dense in its bidual.