Documentation

Mathlib.Topology.UniformSpace.CompactConvergence

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 #

Main results #

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 #

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 KTendstoUniformlyOn (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
Instances For
    @[simp]
    theorem ContinuousMap.toUniformOnFun_toFun {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] (f : C(α, β)) :
    (UniformOnFun.toFun {K : Set α | IsCompact K}) f.toUniformOnFunIsCompact = f

    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₂} [TopologicalSpace α] [UniformSpace β] :
    UniformEmbedding ContinuousMap.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(α, β) | xp.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(α, β) | xp.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(α, β) | xK, (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(α, β) | 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₂} [TopologicalSpace α] [UniformSpace β] {V : Set (β × β)} (K : CompactExhaustion α) (hb : (uniformity β).HasAntitoneBasis V) :
    (uniformity C(α, β)).HasAntitoneBasis fun (n : ) => {fg : C(α, β) × C(α, β) | xK n, (fg.1 x, fg.2 x) V n}

    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) :

    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.uniformContinuous_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : UniformContinuous g) :
    theorem ContinuousMap.uniformInducing_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : UniformInducing g) :
    theorem ContinuousMap.uniformEmbedding_comp {α : Type u₁} {β : Type u₂} [TopologicalSpace α] [UniformSpace β] {δ : Type u_2} [UniformSpace δ] (g : C(β, δ)) (hg : UniformEmbedding g) :
    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.
    Instances For
      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.