# 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 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₂} [] [] (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.

Instances For
theorem ContinuousMap.self_mem_compactConvNhd {α : Type u₁} {β : Type u₂} [] [] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hV : V ) :
theorem ContinuousMap.compactConvNhd_mono {α : Type u₁} {β : Type u₂} [] [] {K : Set α} {V : Set (β × β)} (f : C(α, β)) {V' : Set (β × β)} (hV' : V' V) :
theorem ContinuousMap.compactConvNhd_mem_comp {α : Type u₁} {β : Type u₂} [] [] {K : Set α} {V : Set (β × β)} (f : C(α, β)) {g₁ : C(α, β)} {g₂ : C(α, β)} {V' : Set (β × β)} (hg₁ : g₁ ) (hg₂ : g₂ ) :
theorem ContinuousMap.compactConvNhd_nhd_basis {α : Type u₁} {β : Type u₂} [] [] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hV : V ) :
V', V' V' V ∀ (g : C(α, β)), g

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₂} [] [] (f : C(α, β)) (K₁ : Set α) (K₂ : Set α) (V₁ : Set (β × β)) (V₂ : Set (β × β)) :
ContinuousMap.compactConvNhd (K₁ K₂) (V₁ V₂) f
theorem ContinuousMap.compactConvNhd_compact_entourage_nonempty {α : Type u₁} {β : Type u₂} [] [] :
Set.Nonempty {KV | IsCompact KV.fst KV.snd }
theorem ContinuousMap.compactConvNhd_filter_isBasis {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) :
Filter.IsBasis (fun KV => IsCompact KV.fst KV.snd ) fun KV => ContinuousMap.compactConvNhd KV.fst KV.snd f
def ContinuousMap.compactConvergenceFilterBasis {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) :

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

Instances For
theorem ContinuousMap.mem_compactConvergence_nhd_filter {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) (Y : Set C(α, β)) :
K V _hK _hV,
def ContinuousMap.compactConvergenceTopology {α : Type u₁} {β : Type u₂} [] [] :

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.

Instances For
theorem ContinuousMap.nhds_compactConvergence {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) :
theorem ContinuousMap.hasBasis_nhds_compactConvergence {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) :
Filter.HasBasis (nhds f) (fun p => IsCompact p.fst p.snd ) fun p => ContinuousMap.compactConvNhd p.fst p.snd f
theorem ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn' {α : Type u₁} {β : Type u₂} [] [] (f : C(α, β)) {ι : Type u₃} {p : } {F : ιC(α, β)} :
Filter.Tendsto F p (nhds f) ∀ (K : Set α), 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₂} [] [] {K : Set α} (f : C(α, β)) (hK : ) {U : Set β} (hU : ) (hf : ) :
V, V

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₂} [] [] {K : Set α} {V : Set (β × β)} (f : C(α, β)) (hK : ) (hV : V ) :
ι x C _hC U _hU, f ⋂ (i : ι), ContinuousMap.CompactOpen.gen (C i) (U i) ⋂ (i : ι), ContinuousMap.CompactOpen.gen (C i) (U i)

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₂} [] [] :
ContinuousMap.compactOpen = ContinuousMap.compactConvergenceTopology

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

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

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

Instances For
theorem ContinuousMap.hasBasis_compactConvergenceUniformity_aux {α : Type u₁} {β : Type u₂} [] [] :
Filter.HasBasis ContinuousMap.compactConvergenceUniformity (fun p => IsCompact p.fst p.snd ) fun p => {fg | ∀ (x : α), x p.fst(fg.fst x, fg.snd x) p.snd}
theorem ContinuousMap.mem_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] (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₂} [] [] :

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

theorem ContinuousMap.mem_compactConvergence_entourage_iff {α : Type u₁} {β : Type u₂} [] [] (X : Set (C(α, β) × C(α, β))) :
X K V _hK _hV, {fg | ∀ (x : α), x K(fg.fst x, fg.snd x) V} X
theorem ContinuousMap.hasBasis_compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] :
Filter.HasBasis () (fun p => IsCompact p.fst p.snd ) fun p => {fg | ∀ (x : α), x p.fst(fg.fst x, fg.snd x) p.snd}
theorem Filter.HasBasis.compactConvergenceUniformity {α : Type u₁} {β : Type u₂} [] [] {ι : Type u_1} {pi : ιProp} {s : ιSet (β × β)} (h : Filter.HasBasis () pi s) :
Filter.HasBasis () (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₂} [] [] {f : C(α, β)} {ι : Type u₃} {p : } {F : ιC(α, β)} :
Filter.Tendsto F p (nhds f) ∀ (K : Set α), TendstoUniformlyOn (fun i a => ↑(F i) a) (f) p K
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.hasBasis_compactConvergenceUniformity_of_compact {α : Type u₁} {β : Type u₂} [] [] [] :
Filter.HasBasis () (fun V => V ) fun V => {fg | ∀ (x : α), (fg.fst x, fg.snd 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.