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 its basic properties.

Main definitions

• ContinuousMap.toUniformOnFunIsCompact: natural embedding of C(α, β) into the space α →ᵤ[{K | IsCompact K}] β of all maps α → β with the uniform space structure of uniform convergence on compacts.

• ContinuousMap.compactConvergenceUniformSpace: the UniformSpace structure on C(α, β) induced by the map above.

Main results

• ContinuousMap.mem_compactConvergence_entourage_iff: a characterisation of the entourages of C(α, β).

  The entourages are generated by the following sets. Given K : Set α and V : Set (β × β), let E(K, V) : Set (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 \}. $$ Then the sets E(K, V) for all compact sets K and all entourages V form a basis of entourages of C(α, β).

  As usual, this basis of entourages provides a basis of neighbourhoods by fixing f, see nhds_basis_uniformity'.

• Filter.HasBasis.compactConvergenceUniformity: a similar statement that uses a basis of entourages of β instead of all entourages. It is useful, e.g., if β is a metric space.

• ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn: a sequence of functions Fₙ in C(α, β) converges in the compact-open topology to some f iff Fₙ converges to f uniformly on each compact subset K of α.

• Topology induced by the uniformity described above agrees with the compact-open topology. This is essentially the same as ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn.

  This fact is not available as a separate theorem. Instead, we override the projection of ContinuousMap.compactConvergenceUniformity to TopologicalSpace to be ContinuousMap.compactOpen and prove that they agree, see Note [forgetful inheritance] and implementation notes below.

• ContinuousMap.tendsto_iff_tendstoLocallyUniformly: on a weakly 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

For technical reasons (see Note [forgetful inheritance]), instead of defining a UniformSpace C(α, β) structure and proving in a theorem that it agrees with the compact-open topology, we override the projection right in the definition, so that the resulting instance uses the compact-open topology.

TODO

• Results about uniformly continuous functions γ → C(α, β) and uniform limits of sequences ι → γ → C(α, β).

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

Compact-open topology on C(α, β) agrees with the topology of uniform convergence on compacts: a family of continuous functions F i tends to f in the compact-open topology if and only if the F i tends to f uniformly on all compact sets.

@[deprecated ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn]

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

Alias of ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn.

---

Compact-open topology on C(α, β) agrees with the topology of uniform convergence on compacts: a family of continuous functions F i tends to f in the compact-open topology if and only if the F i tends to f uniformly on all compact sets.

def ContinuousMap.toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : UniformOnFun α β {K : Set α | IsCompact K}

Interpret a bundled continuous map as an element of α →ᵤ[{K | IsCompact K}] β.

We use this map to induce the UniformSpace structure on C(α, β).

Equations

• f.toUniformOnFunIsCompact = (UniformOnFun.ofFun {K : Set α | IsCompact K}) ⇑f

@[simp]

theorem ContinuousMap.toUniformOnFun_toFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) : (UniformOnFun.toFun {K : Set α | IsCompact K}) f.toUniformOnFunIsCompact = ⇑f

theorem ContinuousMap.range_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : Set.range ContinuousMap.toUniformOnFunIsCompact = {f : UniformOnFun α β {K : Set α | IsCompact K} | Continuous f}

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

Uniform space structure on C(α, β).

The uniformity comes from α →ᵤ[{K | IsCompact K}] β (i.e., UniformOnFun α β {K | IsCompact K}) which defines topology of uniform convergence on compact sets. We use ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn to show that the induced topology agrees with the compact-open topology and replace the topology with compactOpen to avoid non-defeq diamonds, see Note [forgetful inheritance].

Equations

• ContinuousMap.compactConvergenceUniformSpace = (UniformSpace.comap ContinuousMap.toUniformOnFunIsCompact inferInstance).replaceTopology ⋯

theorem ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : IsUniformEmbedding ContinuousMap.toUniformOnFunIsCompact

@[deprecated ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact]

theorem ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : IsUniformEmbedding ContinuousMap.toUniformOnFunIsCompact

Alias of ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.

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

theorem ContinuousMap.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] : (uniformity C(α, β)).HasBasis (fun (p : Set α × Set (β × β)) => IsCompact p.1 ∧ p.2 ∈ uniformity β) fun (p : Set α × Set (β × β)) => {fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2}

theorem ContinuousMap.mem_compactConvergence_entourage_iff {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (X : Set (C(α, β) × C(α, β))) : X ∈ uniformity C(α, β) ↔ ∃ (K : Set α) (V : Set (β × β)), IsCompact K ∧ V ∈ uniformity β ∧ {fg : C(α, β) × C(α, β) | ∀ x ∈ K, (fg.1 x, fg.2 x) ∈ V} ⊆ X

theorem CompactExhaustion.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u_1} {p : ι → Prop} {V : ι → Set (β × β)} (K : CompactExhaustion α) (hb : (uniformity β).HasBasis p V) : (uniformity C(α, β)).HasBasis (fun (i : ℕ × ι) => p i.2) fun (i : ℕ × ι) => {fg : C(α, β) × C(α, β) | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2}

If K is a compact exhaustion of α and V i bounded by p i is a basis of entourages of β, then fun (n, i) ↦ {(f, g) | ∀ x ∈ K n, (f x, g x) ∈ V i} bounded by p i is a basis of entourages of C(α, β).

theorem CompactExhaustion.hasAntitoneBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {V : ℕ → Set (β × β)} (K : CompactExhaustion α) (hb : (uniformity β).HasAntitoneBasis V) : (uniformity C(α, β)).HasAntitoneBasis fun (n : ℕ) => {fg : C(α, β) × C(α, β) | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n}

instance ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [WeaklyLocallyCompactSpace α] [SigmaCompactSpace α] [(uniformity β).IsCountablyGenerated] : (uniformity C(α, β)).IsCountablyGenerated

If α is a weakly locally compact σ-compact space (e.g., a proper pseudometric space or a compact spaces) and the uniformity on β is pseudometrizable, then the uniformity on C(α, β) is pseudometrizable too.

Equations

• ⋯ = ⋯

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.

theorem ContinuousMap.uniformContinuous_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : UniformContinuous ⇑g) : UniformContinuous g.comp

theorem ContinuousMap.isUniformInducing_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformInducing ⇑g) : IsUniformInducing g.comp

@[deprecated ContinuousMap.isUniformInducing_comp]

theorem ContinuousMap.uniformInducing_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformInducing ⇑g) : IsUniformInducing g.comp

Alias of ContinuousMap.isUniformInducing_comp.

theorem ContinuousMap.isUniformEmbedding_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformEmbedding ⇑g) : IsUniformEmbedding g.comp

@[deprecated ContinuousMap.isUniformEmbedding_comp]

theorem ContinuousMap.uniformEmbedding_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : IsUniformEmbedding ⇑g) : IsUniformEmbedding g.comp

Alias of ContinuousMap.isUniformEmbedding_comp.

theorem ContinuousMap.uniformContinuous_comp_left {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {γ : Type u_1} [TopologicalSpace γ] (g : C(α, γ)) : UniformContinuous fun (f : C(γ, β)) => f.comp g

def UniformEquiv.arrowCongr {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {γ : Type u_1} {δ : Type u_2} [TopologicalSpace γ] [UniformSpace δ] (φ : α ≃ₜ γ) (ψ : β ≃ᵤ δ) : C(α, β) ≃ᵤ C(γ, δ)

Any pair of a homeomorphism X ≃ₜ Z and an isomorphism Y ≃ᵤ T of uniform spaces gives rise to an isomorphism C(X, Y) ≃ᵤ C(Z, T).

Equations

• One or more equations did not get rendered due to their size.

theorem ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompactSpace α] : (uniformity C(α, β)).HasBasis (fun (V : Set (β × β)) => V ∈ uniformity β) fun (V : Set (β × β)) => {fg : C(α, β) × C(α, β) | ∀ (x : α), (fg.1 x, fg.2 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.

theorem ContinuousMap.uniformSpace_eq_inf_precomp_of_cover {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ₁ : Type u_1} {δ₂ : Type u_2} [TopologicalSpace δ₁] [TopologicalSpace δ₂] (φ₁ : C(δ₁, α)) (φ₂ : C(δ₂, α)) (h_proper₁ : IsProperMap ⇑φ₁) (h_proper₂ : IsProperMap ⇑φ₂) (h_cover : Set.range ⇑φ₁ ∪ Set.range ⇑φ₂ = Set.univ) : inferInstanceAs (UniformSpace C(α, β)) = UniformSpace.comap (fun (x : C(α, β)) => x.comp φ₁) inferInstance ⊓ UniformSpace.comap (fun (x : C(α, β)) => x.comp φ₂) inferInstance

theorem ContinuousMap.uniformSpace_eq_iInf_precomp_of_cover {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {ι : Type u₃} {δ : ι → Type u_1} [(i : ι) → TopologicalSpace (δ i)] (φ : (i : ι) → C(δ i, α)) (h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)) (h_lf : LocallyFinite fun (i : ι) => Set.range ⇑(φ i)) (h_cover : ⋃ (i : ι), Set.range ⇑(φ i) = Set.univ) : inferInstanceAs (UniformSpace C(α, β)) = ⨅ (i : ι), UniformSpace.comap (fun (x : C(α, β)) => x.comp (φ i)) inferInstance

theorem ContinuousMap.completeSpace_of_restrictGenTopology {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] [CompleteSpace β] (h : Topology.RestrictGenTopology {K : Set α | IsCompact K}) : CompleteSpace C(α, β)

If the topology on α is generated by its restrictions to compact sets, then the space of continuous maps C(α, β) is complete (wrt the compact convergence uniformity).

Sufficient conditions on α to satisfy this condition are (weak) local compactness (see ContinuousMap.instCompleteSpaceOfWeaklyLocallyCompactSpace) and sequential compactness (see ContinuousMap.instCompleteSpaceOfSequentialSpace).

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯