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_compact_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_compact_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_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

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

• ContinuousMap.toUniformOnFunIsCompact f = (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}) (ContinuousMap.toUniformOnFunIsCompact f) = ⇑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_compact_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.replaceTopology (UniformSpace.comap ContinuousMap.toUniformOnFunIsCompact inferInstance) ⋯

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

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 : 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 β] : Filter.HasBasis (uniformity C(α, β)) (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 : Filter.HasBasis (uniformity β) p V) : Filter.HasBasis (uniformity C(α, β)) (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 : Filter.HasAntitoneBasis (uniformity β) V) : Filter.HasAntitoneBasis (uniformity C(α, β)) fun (n : ℕ) => {fg : C(α, β) × C(α, β) | ∀ x ∈ K n, (fg.1 x, fg.2 x) ∈ V n}

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

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.

@[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 : 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.