Documentation

TauCeti.Topology.ContinuousMap.ZeroAtInfty.Compactoid

Compactoid subsets of the model spaces C₀(I, K) #

For a discrete index I and a normed field K, a subset S of the model space C₀(I, K) is compactoid exactly when it is bounded and its coordinates decay uniformly: for every ε > 0 there is a finite T ⊆ I with ‖x i‖ < ε for all x ∈ S and i ∉ T (TauCeti.isCompactoidSet_iff_isBounded_and_exists_finset_forall_norm_lt).

Applied to the image of the closed unit ball under an operator between model spaces, uniform coordinate decay is decay of the row norms of its matrix, so this is the set-level half of the identification of operators with compactoid image with operators whose matrix rows tend to zero. Neither completeness, nor discreteness of the valuation, nor the ultrametric inequality is used.

References #

theorem TauCeti.IsCompactoidSet.exists_finset_forall_norm_lt {K : Type u_1} {I : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedField K] {S : Set (ZeroAtInftyContinuousMap I K)} (hS : IsCompactoidSet K S) {ε : ℝ} (hε : 0 < ε) :
∃ (T : Finset I), ∀ x ∈ S, ∀ i ∉ T, ‖x i‖ < ε

The coordinates of a compactoid subset of C₀(I, K) decay uniformly: for every ε > 0 there is a finite T with ‖x i‖ < ε for all x ∈ S and i ∉ T.

theorem TauCeti.isCompactoidSet_iff_isBounded_and_exists_finset_forall_norm_lt {K : Type u_1} {I : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [NormedField K] {S : Set (ZeroAtInftyContinuousMap I K)} :
IsCompactoidSet K S ↔ Bornology.IsBounded S ∧ ∀ (ε : ℝ), 0 < ε → ∃ (T : Finset I), ∀ x ∈ S, ∀ i ∉ T, ‖x i‖ < ε

Compactoid subsets of C₀(I, K): a set is compactoid if and only if it is bounded and its coordinates decay uniformly, i.e. for every ε > 0 there is a finite T with ‖x i‖ < ε for all x ∈ S and i ∉ T.