Approximation by weakly compact sets

Grothendieck's lemma: in a real or complex Banach space, a set A has weakly compact closure as soon as, for every ε > 0, it lies within norm distance ε of some weakly compact set.

The canonical image of A in the bidual then lies in the weak-star compact set J(K) + ε B** for a weakly compact K, so every weak-star cluster point of this image lies within ε of the canonical image J(E). As J(E) is norm closed, these cluster points lie in J(E), and the bidual criterion NormedSpace.isCompact_closure_of_isBounded applies.

This is the standard way to prove weak compactness by truncation: for example, a uniformly integrable subset of L¹ lies within ε of a ball of L², which is weakly compact.

Main statements

• TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact: Grothendieck's lemma.

References

• A. Grothendieck, Sur les applications linéaires faiblement compactes d'espaces du type C(K), Canad. J. Math. 5 (1953), 129–173.
• F. Albiac and N. J. Kalton, Topics in Banach Space Theory, §5.2.

theorem TauCeti.isCompact_closure_toWeakSpace_of_forall_exists_isCompact {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {A : Set E} (h : ∀ ε > 0, ∃ (K : Set E), IsCompact (⇑(toWeakSpace 𝕜 E) '' K) ∧ ∀ x ∈ A, ∃ y ∈ K, ‖x - y‖ ≤ ε) : IsCompact (closure (⇑(toWeakSpace 𝕜 E) '' A))

Grothendieck's lemma. In a real or complex Banach space, a set has weakly compact closure if, for every ε > 0, each of its points lies within norm distance ε of a fixed weakly compact set.