Totally bounded sets lie in the closed convex hull of a null sequence

Grothendieck's compactness lemma: a subset s of a real seminormed space is totally bounded if and only if there is a sequence x : ℕ → E tending to 0 whose range has s inside the closure of its convex hull. In particular every relatively norm-compact set, being totally bounded, lies in the closed convex hull of a null sequence. This is the reduction from compact sets to null sequences used in Grothendieck's characterization of the approximation property by compact operators.

Neither direction needs completeness. Over complex scalars, apply these results to the underlying real space: convexity is real convexity.

Main statements

• TotallyBounded.exists_tendsto_zero_subset_closure_convexHull: a totally bounded set lies in the closed convex hull of the range of a sequence tending to 0.
• TauCeti.totallyBounded_iff_exists_tendsto_zero_subset_closure_convexHull: the converse also holds, so this characterizes totally bounded sets.

References

• A. Grothendieck, Produits tensoriels topologiques et espaces nucléaires, Mem. Amer. Math. Soc. 16 (1955).
• R. E. Megginson, An Introduction to Banach Space Theory, §3.4 (the lemma preceding Grothendieck's approximation property theorem 3.4.32).
• J. Lindenstrauss and L. Tzafriri, Classical Banach Spaces I, §1.e.

theorem TotallyBounded.exists_tendsto_zero_subset_closure_convexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} (hs : TotallyBounded s) : ∃ (x : ℕ → E), Filter.Tendsto x Filter.atTop (nhds 0) ∧ s ⊆ _root_.closure ((convexHull ℝ) (Set.range x))

Grothendieck's compactness lemma. A totally bounded subset of a real seminormed space lies in the closed convex hull of the range of a sequence tending to 0.

theorem TauCeti.totallyBounded_iff_exists_tendsto_zero_subset_closure_convexHull {E : Type u_1} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {s : Set E} : TotallyBounded s ↔ ∃ (x : ℕ → E), Filter.Tendsto x Filter.atTop (nhds 0) ∧ s ⊆ closure ((convexHull ℝ) (Set.range x))

A subset of a real seminormed space is totally bounded if and only if it lies in the closed convex hull of the range of a sequence tending to 0.