Compact convergence (uniform convergence on compact sets) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a topological space α and a uniform space β (e.g., a metric space or a topological group), the space of continuous maps C(α, β) carries a natural uniform space structure. We define this uniform space structure in this file and also prove the following properties of the topology it induces on C(α, β):

1. Given a sequence of continuous functions Fₙ : α → β together with some continuous f : α → β, then Fₙ converges to f as a sequence in C(α, β) iff Fₙ converges to f uniformly on each compact subset K of α.
2. Given Fₙ and f as above and suppose α is locally compact, then Fₙ converges to f iff Fₙ converges to f locally uniformly.
3. The topology coincides with the compact-open topology.

Property 1 is essentially true by definition, 2 follows from basic results about uniform convergence, but 3 requires a little work and uses the Lebesgue number lemma.

The uniform space structure #

Given subsets K ⊆ α and V ⊆ β × β, let E(K, V) ⊆ C(α, β) × C(α, β) be the set of pairs of continuous functions α → β which are V-close on K: $$ E(K, V) = \{ (f, g) | ∀ (x ∈ K), (f x, g x) ∈ V \}. $$ Fixing some f ∈ C(α, β), let N(K, V, f) ⊆ C(α, β) be the set of continuous functions α → β which are V-close to f on K: $$ N(K, V, f) = \{ g | ∀ (x ∈ K), (f x, g x) ∈ V \}. $$ Using this notation we can describe the uniform space structure and the topology it induces. Specifically:

• A subset X ⊆ C(α, β) × C(α, β) is an entourage for the uniform space structure on C(α, β) iff there exists a compact K and entourage V such that E(K, V) ⊆ X.
• A subset Y ⊆ C(α, β) is a neighbourhood of f iff there exists a compact K and entourage V such that N(K, V, f) ⊆ Y.

The topology on C(α, β) thus has a natural subbasis (the compact-open subbasis) and a natural neighbourhood basis (the compact-convergence neighbourhood basis).

Main definitions / results #

• compact_open_eq_compact_convergence: the compact-open topology is equal to the compact-convergence topology.
• compact_convergence_uniform_space: the uniform space structure on C(α, β).
• mem_compact_convergence_entourage_iff: a characterisation of the entourages of C(α, β).
• tendsto_iff_forall_compact_tendsto_uniformly_on: a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly on each compact subset K of α.
• tendsto_iff_tendsto_locally_uniformly: on a locally compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f locally uniformly.
• tendsto_iff_tendsto_uniformly: on a compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly.

Implementation details #

We use the forgetful inheritance pattern (see Note [forgetful inheritance]) to make the topology of the uniform space structure on C(α, β) definitionally equal to the compact-open topology.

TODO #

• When β is a metric space, there is natural basis for the compact-convergence topology parameterised by triples (K, ε, f) for a real number ε > 0.
• When α is compact and β is a metric space, the compact-convergence topology (and thus also the compact-open topology) is metrisable.
• Results about uniformly continuous functions γ → C(α, β) and uniform limits of sequences ι → γ → C(α, β).