Compact convergence (uniform convergence on compact sets)

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

• ContinuousMap.compactOpen_eq_compactConvergence: the compact-open topology is equal to the compact-convergence topology.
• ContinuousMap.compactConvergenceUniformSpace: the uniform space structure on C(α, β).
• ContinuousMap.mem_compactConvergence_entourage_iff: a characterisation of the entourages of C(α, β).
• ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn: a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f uniformly on each compact subset K of α.
• ContinuousMap.tendsto_iff_tendstoLocallyUniformly: on a locally compact space, a sequence of functions Fₙ in C(α, β) converges to some f iff Fₙ converges to f locally uniformly.
• ContinuousMap.tendsto_iff_tendstoUniformly: 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(α, β).

def ContinuousMap.compactConvNhd {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (K : Set α) (V : Set (β × β)) (f : C(α, β)) : Set C(α, β)

Given K ⊆ α, V ⊆ β × β, and f : C(α, β), we define ContinuousMap.compactConvNhd K V f to be the set of g : C(α, β) that are V-close to f on K.

theorem ContinuousMap.self_mem_compactConvNhd {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hV : V ∈ uniformity β) : f ∈ ContinuousMap.compactConvNhd K V f

theorem ContinuousMap.compactConvNhd_mono {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} {V : Set (β × β)} (f : C(α, β)) {V' : Set (β × β)} (hV' : V' ⊆ V) : ContinuousMap.compactConvNhd K V' f ⊆ ContinuousMap.compactConvNhd K V f

theorem ContinuousMap.compactConvNhd_mem_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} {V : Set (β × β)} (f : C(α, β)) {g₁ : C(α, β)} {g₂ : C(α, β)} {V' : Set (β × β)} (hg₁ : g₁ ∈ ContinuousMap.compactConvNhd K V f) (hg₂ : g₂ ∈ ContinuousMap.compactConvNhd K V' g₁) : g₂ ∈ ContinuousMap.compactConvNhd K (compRel V V') f

theorem ContinuousMap.compactConvNhd_nhd_basis {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hV : V ∈ uniformity β) : ∃ V', V' ∈ uniformity β ∧ V' ⊆ V ∧ ∀ (g : C(α, β)), g ∈ ContinuousMap.compactConvNhd K V' f → ContinuousMap.compactConvNhd K V' g ⊆ ContinuousMap.compactConvNhd K V f

A key property of ContinuousMap.compactConvNhd. It allows us to apply TopologicalSpace.nhds_mkOfNhds_filterBasis below.

theorem ContinuousMap.compactConvNhd_subset_inter {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) (K₁ : Set α) (K₂ : Set α) (V₁ : Set (β × β)) (V₂ : Set (β × β)) : ContinuousMap.compactConvNhd (K₁ ∪ K₂) (V₁ ∩ V₂) f ⊆ ContinuousMap.compactConvNhd K₁ V₁ f ∩ ContinuousMap.compactConvNhd K₂ V₂ f

theorem ContinuousMap.compactConvNhd_compact_entourage_nonempty {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Set.Nonempty {KV | IsCompact KV.fst ∧ KV.snd ∈ uniformity β}

theorem ContinuousMap.compactConvNhd_filter_isBasis {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : Filter.IsBasis (fun KV => IsCompact KV.fst ∧ KV.snd ∈ uniformity β) fun KV => ContinuousMap.compactConvNhd KV.fst KV.snd f

def ContinuousMap.compactConvergenceFilterBasis {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : FilterBasis C(α, β)

A filter basis for the neighbourhood filter of a point in the compact-convergence topology.

theorem ContinuousMap.mem_compactConvergence_nhd_filter {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) (Y : Set C(α, β)) : Y ∈ FilterBasis.filter (ContinuousMap.compactConvergenceFilterBasis f) ↔ ∃ K V _hK _hV, ContinuousMap.compactConvNhd K V f ⊆ Y

def ContinuousMap.compactConvergenceTopology {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : TopologicalSpace C(α, β)

The compact-convergence topology. In fact, see ContinuousMap.compactOpen_eq_compactConvergence this is the same as the compact-open topology. This definition is thus an auxiliary convenience definition and is unlikely to be of direct use.

theorem ContinuousMap.nhds_compactConvergence {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : nhds f = FilterBasis.filter (ContinuousMap.compactConvergenceFilterBasis f)

theorem ContinuousMap.hasBasis_nhds_compactConvergence {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : Filter.HasBasis (nhds f) (fun p => IsCompact p.fst ∧ p.snd ∈ uniformity β) fun p => ContinuousMap.compactConvNhd p.fst p.snd f

theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn' {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} : Filter.Tendsto F p (nhds f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K

This is an auxiliary lemma and is unlikely to be of direct use outside of this file. See ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn below for the useful version where the topology is picked up via typeclass inference.

theorem ContinuousMap.compactConvNhd_subset_compactOpen {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} (f : C(α, β)) (hK : IsCompact K) {U : Set β} (hU : IsOpen U) (hf : f ∈ ContinuousMap.CompactOpen.gen K U) : ∃ V, V ∈ uniformity β ∧ IsOpen V ∧ ContinuousMap.compactConvNhd K V f ⊆ ContinuousMap.CompactOpen.gen K U

Any point of ContinuousMap.CompactOpen.gen K U is also an interior point wrt the topology of compact convergence.

The topology of compact convergence is thus at least as fine as the compact-open topology.

theorem ContinuousMap.iInter_compactOpen_gen_subset_compactConvNhd {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hK : IsCompact K) (hV : V ∈ uniformity β) : ∃ ι x C _hC U _hU, f ∈ ⋂ (i : ι), ContinuousMap.CompactOpen.gen (C i) (U i) ∧ ⋂ (i : ι), ContinuousMap.CompactOpen.gen (C i) (U i) ⊆ ContinuousMap.compactConvNhd K V f

The point f in ContinuousMap.compactConvNhd K V f is also an interior point wrt the compact-open topology.

Since ContinuousMap.compactConvNhd K V f are a neighbourhood basis at f for each f, it follows that the compact-open topology is at least as fine as the topology of compact convergence.

theorem ContinuousMap.compactOpen_eq_compactConvergence {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : ContinuousMap.compactOpen = ContinuousMap.compactConvergenceTopology

The compact-open topology is equal to the compact-convergence topology.

def ContinuousMap.compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Filter (C(α, β) × C(α, β))

The filter on C(α, β) × C(α, β) which underlies the uniform space structure on C(α, β).

theorem ContinuousMap.hasBasis_compactConvergenceUniformity_aux {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Filter.HasBasis ContinuousMap.compactConvergenceUniformity (fun p => IsCompact p.fst ∧ p.snd ∈ uniformity β) fun p => {fg | ∀ (x : α), x ∈ p.fst → (↑fg.fst x, ↑fg.snd x) ∈ p.snd}

theorem ContinuousMap.mem_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (X : Set (C(α, β) × C(α, β))) : X ∈ ContinuousMap.compactConvergenceUniformity ↔ ∃ K V _hK _hV, {fg | ∀ (x : α), x ∈ K → (↑fg.fst x, ↑fg.snd x) ∈ V} ⊆ X

An intermediate lemma. Usually ContinuousMap.mem_compactConvergence_entourage_iff is more useful.

instance ContinuousMap.compactConvergenceUniformSpace {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : UniformSpace C(α, β)

Note that we ensure the induced topology is definitionally the compact-open topology.

theorem ContinuousMap.mem_compactConvergence_entourage_iff {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (X : Set (C(α, β) × C(α, β))) : X ∈ uniformity C(α, β) ↔ ∃ K V _hK _hV, {fg | ∀ (x : α), x ∈ K → (↑fg.fst x, ↑fg.snd x) ∈ V} ⊆ X

theorem ContinuousMap.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Filter.HasBasis (uniformity C(α, β)) (fun p => IsCompact p.fst ∧ p.snd ∈ uniformity β) fun p => {fg | ∀ (x : α), x ∈ p.fst → (↑fg.fst x, ↑fg.snd x) ∈ p.snd}

theorem Filter.HasBasis.compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u_1} {pi : ι → Prop} {s : ι → Set (β × β)} (h : Filter.HasBasis (uniformity β) pi s) : Filter.HasBasis (uniformity C(α, β)) (fun p => IsCompact p.fst ∧ pi p.snd) fun p => {fg | ∀ (x : α), x ∈ p.fst → (↑fg.fst x, ↑fg.snd x) ∈ s p.snd}

theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} : Filter.Tendsto F p (nhds f) ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn (fun i a => ↑(F i) a) (↑f) p K

theorem ContinuousMap.tendsto_of_tendstoLocallyUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} (h : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p) : Filter.Tendsto F p (nhds f)

Locally uniform convergence implies convergence in the compact-open topology.

theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} [WeaklyLocallyCompactSpace α] : Filter.Tendsto F p (nhds f) ↔ TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p

In a weakly locally compact space, convergence in the compact-open topology is the same as locally uniform convergence.

The right-to-left implication holds in any topological space, see ContinuousMap.tendsto_of_tendstoLocallyUniformly.

@[deprecated ContinuousMap.tendsto_iff_tendstoLocallyUniformly]

theorem ContinuousMap.tendstoLocallyUniformly_of_tendsto {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} [WeaklyLocallyCompactSpace α] (h : Filter.Tendsto F p (nhds f)) : TendstoLocallyUniformly (fun i a => ↑(F i) a) (↑f) p

theorem ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] : Filter.HasBasis (uniformity C(α, β)) (fun V => V ∈ uniformity β) fun V => {fg | ∀ (x : α), (↑fg.fst x, ↑fg.snd x) ∈ V}

theorem ContinuousMap.tendsto_iff_tendstoUniformly {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {f : C(α, β)} {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} [CompactSpace α] : Filter.Tendsto F p (nhds f) ↔ TendstoUniformly (fun i a => ↑(F i) a) (↑f) p

Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space.