Reflexivity and weak compactness

A real or complex seminormed space is reflexive if and only if its closed unit ball is weakly compact. More generally, every norm-closed bounded real-convex set in a reflexive space is weakly compact. This rests on TauCeti.isCompact_closure_toWeakSpace from TauCeti.Analysis.Normed.Module.DoubleDual: over any proper nontrivially normed field, every bounded set in a reflexive space has weakly compact closure.

Reflexivity means surjectivity of NormedSpace.inclusionInDoubleDual. No completeness, separability or separation hypothesis is needed for the equivalence. For normed spaces, either condition also implies completeness. The topology changes are explicit, using toWeakSpace and NormedSpace.inclusionInDoubleDualWeak.

The forward direction transports Banach–Alaoglu along the inducing bidual map; the reverse direction uses Goldstine's theorem.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §2.6.

theorem TauCeti.surjective_inclusionInDoubleDual_of_isCompact_toWeakSpace_closedBall {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (hball : IsCompact (⇑(toWeakSpace 𝕜 E) '' Metric.closedBall 0 1)) : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)

A seminormed space whose closed unit ball is weakly compact is reflexive.

theorem TauCeti.isCompact_toWeakSpace_of_isClosed_of_convex_of_isBounded {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (hE : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)) [Module ℝ E] [IsScalarTower ℝ 𝕜 E] {s : Set E} (hclosed : IsClosed s) (hconv : Convex ℝ s) (hbound : Bornology.IsBounded s) : IsCompact (⇑(toWeakSpace 𝕜 E) '' s)

Norm-closed bounded real-convex subsets of a reflexive seminormed space are weakly compact. Convexity over real scalars also covers complex seminormed spaces.

theorem TauCeti.isCompact_toWeakSpace_closedBall {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (hE : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E)) (x : E) (r : ℝ) : IsCompact (⇑(toWeakSpace 𝕜 E) '' Metric.closedBall x r)

Every closed ball in a reflexive seminormed space is weakly compact, including balls of zero or negative radius.

theorem TauCeti.surjective_inclusionInDoubleDual_iff_isCompact_toWeakSpace_closedBall {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Function.Surjective ⇑(NormedSpace.inclusionInDoubleDual 𝕜 E) ↔ IsCompact (⇑(toWeakSpace 𝕜 E) '' Metric.closedBall 0 1)

A real or complex seminormed space is reflexive exactly when its closed unit ball is weakly compact. No completeness or separation assumption is needed.