# 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₂} [] [] {ι : Type u₃} {p : } {F : ιC(α, β)} {f : C(α, β)} :
Filter.Tendsto F p (nhds f) ∀ (K : Set α), 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₂} [] [] (f : C(α, β)) :
UniformOnFun α β {K : Set α | }

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

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

Equations
Instances For
@[simp]
theorem ContinuousMap.toUniformOnFun_toFun {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) :
(UniformOnFun.toFun {K : Set α | }) f.toUniformOnFunIsCompact = f
instance ContinuousMap.compactConvergenceUniformSpace {α : Type u₁} {β : Type u₂} [] [] :

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.comap ContinuousMap.toUniformOnFunIsCompact inferInstance).replaceTopology
theorem ContinuousMap.uniformEmbedding_toUniformOnFunIsCompact {α : Type u₁} {β : Type u₂} [] [] :
UniformEmbedding ContinuousMap.toUniformOnFunIsCompact
theorem Filter.HasBasis.compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] {ι : Type u_1} {pi : ιProp} {s : ιSet (β × β)} (h : ().HasBasis pi s) :
().HasBasis (fun (p : Set α × ι) => IsCompact p.1 pi p.2) fun (p : Set α × ι) => {fg : C(α, β) × C(α, β) | xp.1, (fg.1 x, fg.2 x) s p.2}
theorem ContinuousMap.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] :
().HasBasis (fun (p : Set α × Set (β × β)) => IsCompact p.1 p.2 ) fun (p : Set α × Set (β × β)) => {fg : C(α, β) × C(α, β) | xp.1, (fg.1 x, fg.2 x) p.2}
theorem ContinuousMap.mem_compactConvergence_entourage_iff {α : Type u₁} {β : Type u₂} [] [] (X : Set (C(α, β) × C(α, β))) :
X ∃ (K : Set α) (V : Set (β × β)), V {fg : C(α, β) × C(α, β) | xK, (fg.1 x, fg.2 x) V} X
theorem CompactExhaustion.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] {ι : Type u_1} {p : ιProp} {V : ιSet (β × β)} (K : ) (hb : ().HasBasis p V) :
().HasBasis (fun (i : × ι) => p i.2) fun (i : × ι) => {fg : C(α, β) × C(α, β) | xK 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₂} [] [] {V : Set (β × β)} (K : ) (hb : ().HasAntitoneBasis V) :
().HasAntitoneBasis fun (n : ) => {fg : C(α, β) × C(α, β) | xK n, (fg.1 x, fg.2 x) V n}
instance ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace {α : Type u₁} {β : Type u₂} [] [] [().IsCountablyGenerated] :
().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₂} [] [] {f : C(α, β)} {ι : Type u₃} {p : } {F : ιC(α, β)} (h : TendstoLocallyUniformly (fun (i : ι) (a : α) => (F i) a) (f) p) :

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

theorem ContinuousMap.tendsto_iff_tendstoLocallyUniformly {α : Type u₁} {β : Type u₂} [] [] {f : C(α, β)} {ι : Type u₃} {p : } {F : ιC(α, β)} :
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₂} [] [] {f : C(α, β)} {ι : Type u₃} {p : } {F : ιC(α, β)} (h : Filter.Tendsto F p (nhds f)) :
TendstoLocallyUniformly (fun (i : ι) (a : α) => (F i) a) (f) p
theorem ContinuousMap.uniformContinuous_comp {α : Type u₁} {β : Type u₂} [] [] {δ : Type u_2} [] (g : C(β, δ)) (hg : ) :
theorem ContinuousMap.uniformInducing_comp {α : Type u₁} {β : Type u₂} [] [] {δ : Type u_2} [] (g : C(β, δ)) (hg : ) :
theorem ContinuousMap.uniformEmbedding_comp {α : Type u₁} {β : Type u₂} [] [] {δ : Type u_2} [] (g : C(β, δ)) (hg : ) :
theorem ContinuousMap.uniformContinuous_comp_left {α : Type u₁} {β : Type u₂} [] [] {γ : Type u_1} [] (g : C(α, γ)) :
UniformContinuous fun (f : C(γ, β)) => f.comp g
def UniformEquiv.arrowCongr {α : Type u₁} {β : Type u₂} [] [] {γ : Type u_1} {δ : Type u_2} [] [] (φ : α ≃ₜ γ) (ψ : β ≃ᵤ δ) :
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.
Instances For
theorem ContinuousMap.hasBasis_compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [] [] [] :
().HasBasis (fun (V : Set (β × β)) => V ) fun (V : Set (β × β)) => {fg : C(α, β) × C(α, β) | ∀ (x : α), (fg.1 x, fg.2 x) V}
theorem ContinuousMap.tendsto_iff_tendstoUniformly {α : Type u₁} {β : Type u₂} [] [] {f : C(α, β)} {ι : Type u₃} {p : } {F : ιC(α, β)} [] :
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.