Compactoid subsets of normed spaces

A subset S of a seminormed space E over a normed field K is compactoid (TauCeti.IsCompactoidSet K S) if for every ε > 0 there are finitely many vectors v₁, …, vₙ such that every x ∈ S lies within ε of a combination ∑ aᵢ • vᵢ with all ‖aᵢ‖ ≤ 1. Over a nonarchimedean field the combinations with ‖aᵢ‖ ≤ 1 are exactly the K°-submodule spanned by the vᵢ, so this is the condition that S ⊆ U + span_{K°} F for every zero neighbourhood U and some finite F (TauCeti.isCompactoidSet_iff_forall_mem_nhds).

Compactoid sets replace relatively compact sets in nonarchimedean functional analysis: over a field such as ℂ_p, which is not locally compact, a bounded subset of a line need not be totally bounded, yet it is compactoid. Operators mapping the closed unit ball to a compactoid set are the compact operators of nonarchimedean Banach space theory. Every totally bounded set is compactoid, and over a field whose closed balls are compact, such as a nontrivially normed locally compact field, the two notions agree (TauCeti.isCompactoidSet_iff_totallyBounded).

Main definitions

• TauCeti.IsCompactoidSet K S: finite approximation of S by combinations with coefficients in the closed unit ball of K.

Main results

• TauCeti.isCompactoidSet_iff_forall_mem_nhds: the formulation through zero neighbourhoods.
• TauCeti.isCompactoidSet_of_forall_exists_finset: approximation by finite subfamilies of a fixed family suffices.
• TauCeti.IsCompactoidSet.exists_seq_forall_exists_finset: conversely, a compactoid set is approximated by finite pieces of one sequence.
• TauCeti.isCompactoidSet_of_forall_exists_norm_sub_lt: a set approximated arbitrarily well by compactoid sets is compactoid.
• TauCeti.IsCompactoidSet.mono, TauCeti.IsCompactoidSet.union, TauCeti.IsCompactoidSet.add, TauCeti.isCompactoidSet_sum, TauCeti.IsCompactoidSet.smul, TauCeti.IsCompactoidSet.image, TauCeti.isCompactoidSet_closure_iff: stability under subsets, finite unions, finite sums, scalar multiples, continuous linear images and closure.
• TotallyBounded.isCompactoidSet, Set.Finite.isCompactoidSet: totally bounded sets, in particular finite sets, are compactoid.
• TauCeti.IsCompactoidSet.isBounded: compactoid sets are bounded.
• Bornology.IsBounded.isCompactoidSet: in a finite-dimensional space over a complete nontrivially normed field, conversely, bounded sets are compactoid.
• TauCeti.isCompactoidSet_iff_totallyBounded: over a field whose closed balls are compact, compactoid sets are exactly the totally bounded sets.

References

• N. De Grande-De Kimpe, Non-archimedean nuclearity, Groupe de travail d'analyse ultramétrique 9, no. 3 (1981–1982), exp. J4, §§1.1, 2.1.
• W. H. Schikhof, Banach spaces over nonarchimedean valued fields, Topology Proceedings 24 (1999), 547–581, §§2.13, 2.15.

def TauCeti.IsCompactoidSet (K : Type u_1) {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] (S : Set E) : Prop

A subset S of a seminormed K-space is compactoid if for every ε > 0 there are finitely many vectors v i such that every x ∈ S is within ε of some ∑ i, a i • v i with all ‖a i‖ ≤ 1.

theorem TauCeti.isCompactoidSet_iff {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} : IsCompactoidSet K S ↔ ∀ (ε : ℝ), 0 < ε → ∃ (n : ℕ) (v : Fin n → E), ∀ x ∈ S, ∃ (a : Fin n → K), (∀ (i : Fin n), ‖a i‖ ≤ 1) ∧ ‖x - ∑ i : Fin n, a i • v i‖ < ε

Unfolding TauCeti.IsCompactoidSet.

theorem TauCeti.isCompactoidSet_iff_forall_mem_nhds {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} : IsCompactoidSet K S ↔ ∀ U ∈ nhds 0, ∃ (n : ℕ) (v : Fin n → E), ∀ x ∈ S, ∃ (a : Fin n → K), (∀ (i : Fin n), ‖a i‖ ≤ 1) ∧ x - ∑ i : Fin n, a i • v i ∈ U

A set is compactoid if and only if for every neighbourhood U of zero there are finitely many vectors v i with S ⊆ U + {∑ i, a i • v i | ‖a i‖ ≤ 1}.

theorem TauCeti.isCompactoidSet_of_forall_exists_finset {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {ι : Type u_4} {S : Set E} (v : ι → E) (h : ∀ (ε : ℝ), 0 < ε → ∃ (t : Finset ι), ∀ x ∈ S, ∃ (a : ι → K), (∀ (i : ι), ‖a i‖ ≤ 1) ∧ ‖x - ∑ i ∈ t, a i • v i‖ < ε) : IsCompactoidSet K S

To show that S is compactoid it suffices to approximate it, for every ε > 0, by combinations of a finite subfamily of a fixed family v, with coefficients of norm at most one.

theorem TauCeti.IsCompactoidSet.exists_seq_forall_exists_finset {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : IsCompactoidSet K S) : ∃ (v : ℕ → E), ∀ (ε : ℝ), 0 < ε → ∃ (t : Finset ℕ), ∀ x ∈ S, ∃ (a : ℕ → K), (∀ (i : ℕ), ‖a i‖ ≤ 1) ∧ ‖x - ∑ i ∈ t, a i • v i‖ < ε

A compactoid set is approximated by finite pieces of one sequence: there is a sequence v such that, for every ε > 0, every point of S is within ε of a combination of finitely many fixed terms of v with coefficients of norm at most one. Consequently S lies in the closure of the span of v.

theorem TauCeti.IsCompactoidSet.mono {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S T : Set E} (hT : IsCompactoidSet K T) (hST : S ⊆ T) : IsCompactoidSet K S

A subset of a compactoid set is compactoid.

@[simp]

theorem TauCeti.isCompactoidSet_empty {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] : IsCompactoidSet K ∅

The empty set is compactoid.

theorem TauCeti.IsCompactoidSet.union {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S T : Set E} (hS : IsCompactoidSet K S) (hT : IsCompactoidSet K T) : IsCompactoidSet K (S ∪ T)

The union of two compactoid sets is compactoid.

theorem TauCeti.IsCompactoidSet.add {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S T : Set E} (hS : IsCompactoidSet K S) (hT : IsCompactoidSet K T) : IsCompactoidSet K (S + T)

The pointwise sum of two compactoid sets is compactoid.

theorem TauCeti.isCompactoidSet_sum {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {ι : Type u_4} {s : Finset ι} (t : ι → Set E) (h : ∀ i ∈ s, IsCompactoidSet K (t i)) : IsCompactoidSet K (∑ i ∈ s, t i)

A finite pointwise sum of compactoid sets is compactoid.

theorem TauCeti.isCompactoidSet_of_forall_exists_norm_sub_lt {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (h : ∀ (ε : ℝ), 0 < ε → ∃ (T : Set E), IsCompactoidSet K T ∧ ∀ x ∈ S, ∃ y ∈ T, ‖x - y‖ < ε) : IsCompactoidSet K S

A set that lies, for every ε > 0, within distance ε of some compactoid set is compactoid.

theorem TauCeti.IsCompactoidSet.closure {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : IsCompactoidSet K S) : IsCompactoidSet K (_root_.closure S)

The closure of a compactoid set is compactoid.

@[simp]

theorem TauCeti.isCompactoidSet_closure_iff {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} : IsCompactoidSet K (closure S) ↔ IsCompactoidSet K S

A set is compactoid if and only if its closure is.

theorem TauCeti.IsCompactoidSet.isBounded {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : IsCompactoidSet K S) : Bornology.IsBounded S

A compactoid set is bounded.

theorem TauCeti.IsCompactoidSet.image {K : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [SeminormedAddCommGroup F] [NormedSpace K F] {S : Set E} (hS : IsCompactoidSet K S) (u : E →L[K] F) : IsCompactoidSet K (⇑u '' S)

The image of a compactoid set under a continuous linear map is compactoid.

theorem TauCeti.IsCompactoidSet.smul {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : IsCompactoidSet K S) (c : K) : IsCompactoidSet K (c • S)

A scalar multiple of a compactoid set is compactoid.

theorem TauCeti.IsCompactoidSet.totallyBounded {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [ProperSpace K] {S : Set E} (hS : IsCompactoidSet K S) : TotallyBounded S

Over a field whose closed balls are compact, for instance a nontrivially normed locally compact field such as ℚ_p, every compactoid set is totally bounded.

theorem Bornology.IsBounded.isCompactoidSet {K : Type u_1} {E : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E] [NormedSpace K E] [FiniteDimensional K E] {S : Set E} (hS : IsBounded S) : TauCeti.IsCompactoidSet K S

A bounded subset of a finite-dimensional normed space over a complete nontrivially normed field is compactoid: after scaling by a scalar of large norm, its coordinates in a basis have norm at most one.

theorem TotallyBounded.isCompactoidSet {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : TotallyBounded S) : TauCeti.IsCompactoidSet K S

A totally bounded set is compactoid.

theorem Set.Finite.isCompactoidSet {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : S.Finite) : TauCeti.IsCompactoidSet K S

A finite set is compactoid.

theorem IsCompact.isCompactoidSet {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] {S : Set E} (hS : IsCompact S) : TauCeti.IsCompactoidSet K S

A compact set is compactoid.

theorem TauCeti.isCompactoidSet_iff_totallyBounded {K : Type u_1} {E : Type u_2} [NormedField K] [SeminormedAddCommGroup E] [NormedSpace K E] [ProperSpace K] {S : Set E} : IsCompactoidSet K S ↔ TotallyBounded S

Over a field whose closed balls are compact, a set is compactoid if and only if it is totally bounded.