The Krein–Šmulian theorem

The Krein–Šmulian theorem says that a convex subset C of the dual of a Banach space E is weak-star closed as soon as its intersection with every closed ball centred at zero is weak-star closed. For a linear subspace it suffices that its intersection with the closed unit ball is weak-star closed.

The heart of the theorem is a separation statement: if C is convex, has weak-star closed bounded slices, and avoids the closed ball of radius r > 0, then a single point x of E satisfies 1 ≤ re (f x) for every f ∈ C, so that the weak-star continuous functional of evaluation at x separates C from zero.

Main results

• IsCompact.exists_finset_forall_one_lt_re_apply: finitely many points of norm at most ρ⁻¹ push a weak-star compact set of functionals of norm greater than ρ above the real level one.
• Convex.exists_forall_one_le_re_apply_of_tendsto: if every functional in a convex set reaches real level one somewhere along a null family of points of a Banach space, a single point does it for all of them.
• Convex.exists_forall_one_le_re_apply: the separation statement above.
• Convex.isClosed_iff_forall_isClosed_inter_closedBall: the Krein–Šmulian theorem.
• Submodule.isClosed_iff_isClosed_inter_closedBall_zero_one: its form for subspaces.

References

• R. E. Megginson, An Introduction to Banach Space Theory, Theorem 2.7.11.
• J. B. Conway, A Course in Functional Analysis, Theorem V.12.1.

theorem IsCompact.exists_finset_forall_one_lt_re_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Set (WeakDual 𝕜 E)} (hS : IsCompact S) {ρ : ℝ} (hρ : 0 < ρ) (hSρ : ∀ f ∈ S, ρ < ‖WeakDual.toStrongDual f‖) : ∃ (F : Finset E), (∀ x ∈ F, ‖x‖ ≤ ρ⁻¹) ∧ ∀ f ∈ S, ∃ x ∈ F, 1 < RCLike.re (f x)

A weak-star compact set of functionals of norm greater than ρ > 0 is pushed above the real level one by finitely many points of norm at most ρ⁻¹.

theorem Convex.exists_forall_one_le_re_apply_of_tendsto {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {C : Set (WeakDual 𝕜 E)} (hC : Convex ℝ C) {ι : Type u_3} {v : ι → E} (hv : Filter.Tendsto v Filter.cofinite (nhds 0)) (hCv : ∀ f ∈ C, ∃ (i : ι), 1 ≤ RCLike.re (f (v i))) : ∃ (x : E), ∀ f ∈ C, 1 ≤ RCLike.re (f x)

If every functional in a convex set C has real part at least one somewhere along a null family v of points of a Banach space, then evaluation at a single point x satisfies 1 ≤ re (f x) for all f ∈ C.

theorem Convex.exists_forall_one_le_re_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {C : Set (WeakDual 𝕜 E)} (hC : Convex ℝ C) (hCR : ∀ (R : ℝ), IsClosed (C ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 R)) {r : ℝ} (hr : 0 < r) (hCr : ∀ f ∈ C, r < ‖WeakDual.toStrongDual f‖) : ∃ (x : E), ∀ f ∈ C, 1 ≤ RCLike.re (f x)

Separation lemma of the Krein–Šmulian theorem. Let C be a convex set of functionals on a Banach space whose intersection with every closed ball centred at zero is weak-star closed. If every element of C has norm greater than some r > 0, then evaluation at a single point x separates C from zero: 1 ≤ re (f x) for every f ∈ C.

theorem Convex.isClosed_iff_forall_isClosed_inter_closedBall {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {C : Set (WeakDual 𝕜 E)} (hC : Convex ℝ C) : IsClosed C ↔ ∀ (r : ℝ), IsClosed (C ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 r)

Krein–Šmulian theorem. A convex subset of the dual of a Banach space is weak-star closed if and only if its intersection with every closed ball centred at zero is weak-star closed.

theorem Submodule.isClosed_iff_isClosed_inter_closedBall_zero_one {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (G : Submodule 𝕜 (WeakDual 𝕜 E)) : IsClosed ↑G ↔ IsClosed (↑G ∩ ⇑WeakDual.toStrongDual ⁻¹' Metric.closedBall 0 1)

Krein–Šmulian theorem for subspaces. A subspace of the dual of a Banach space is weak-star closed if and only if its intersection with the closed unit ball is weak-star closed.