Weakly compact sets are weakly sequentially compact

This file proves Šmulian's half of the Eberlein–Šmulian theorem: in a real or complex normed space, a weakly compact set is weakly sequentially compact, and every sequence in a relatively weakly compact set has a weakly convergent subsequence. No separability or completeness assumption is made on the space.

The proof is a separable reduction. A norm-separable set s is separated by countably many continuous linear functionals of norm at most one: choose norming functionals at the points of a countable dense subset of s - s. On a weakly compact, norm-separable set these functionals induce a continuous injection into a countable product of metric spaces, so the weak topology there is metrizable and compactness gives convergent subsequences. A sequence in an arbitrary weakly compact set K lies in the closed linear span of its terms, which is norm separable and, being convex and norm closed, weakly closed; its intersection with K is therefore a weakly compact, norm-separable set containing the sequence.

The separation argument is the one carried out inline in Mathlib's ae_eq_zero_of_forall_dual_of_isSeparable, and the metrizability step follows Mathlib's WeakDual.metrizable_of_isCompact for the weak-star topology.

Main declarations

• TauCeti.exists_seq_dual_injOn_of_isSeparable: countably many functionals of norm at most one separate the points of a norm-separable set.
• TauCeti.metrizableSpace_toWeakSpace_of_isSeparable_of_isCompact: a weakly compact, norm-separable set is metrizable in the weak topology.
• TauCeti.isSeqCompact_toWeakSpace_of_isCompact: weakly compact sets are weakly sequentially compact.
• TauCeti.tendsto_subseq_toWeakSpace_of_isCompact_closure: every sequence in a relatively weakly compact set has a subsequence converging weakly to a point of the space.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §2.8 (Theorem 2.8.6).
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §1.6.

theorem TauCeti.exists_seq_dual_injOn_of_isSeparable (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (hs : TopologicalSpace.IsSeparable s) : ∃ (f : ℕ → StrongDual 𝕜 E), (∀ (n : ℕ), ‖f n‖ ≤ 1) ∧ Set.InjOn (fun (x : E) (n : ℕ) => (f n) x) s

Countably many continuous linear functionals of norm at most one separate the points of a norm-separable set.

theorem TauCeti.metrizableSpace_toWeakSpace_of_isSeparable_of_isCompact {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {K : Set E} (hsep : TopologicalSpace.IsSeparable K) (hK : IsCompact (⇑(toWeakSpace 𝕜 E) '' K)) : TopologicalSpace.MetrizableSpace ↑(⇑(toWeakSpace 𝕜 E) '' K)

A weakly compact, norm-separable set is metrizable in the weak topology.

theorem TauCeti.isSeqCompact_toWeakSpace_of_isCompact {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {K : Set E} (hK : IsCompact (⇑(toWeakSpace 𝕜 E) '' K)) : IsSeqCompact (⇑(toWeakSpace 𝕜 E) '' K)

Šmulian's theorem: in a real or complex normed space, a weakly compact set is weakly sequentially compact. Neither completeness nor separability of the space is assumed.

theorem TauCeti.tendsto_subseq_toWeakSpace_of_isCompact_closure {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {K : Set E} (hK : IsCompact (closure (⇑(toWeakSpace 𝕜 E) '' K))) {u : ℕ → E} (hu : ∀ (n : ℕ), u n ∈ K) : ∃ (x : E) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (fun (n : ℕ) => (toWeakSpace 𝕜 E) (u (φ n))) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x))

Šmulian's theorem, relative form: every sequence in a relatively weakly compact subset of a real or complex normed space has a subsequence converging weakly to some point of the space.