mathlib3 documentation

topology.uniform_space.compact_convergence

Compact convergence (uniform convergence on compact sets) #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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:

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 #

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 #

def continuous_map.compact_conv_nhd {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (K : set α) (V : set × β)) (f : C(α, β)) :
set C(α, β)

Given K ⊆ α, V ⊆ β × β, and f : C(α, β), we define compact_conv_nhd K V f to be the set of g : C(α, β) that are V-close to f on K.

Equations
theorem continuous_map.self_mem_compact_conv_nhd {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} {V : set × β)} (f : C(α, β)) (hV : V uniformity β) :
theorem continuous_map.compact_conv_nhd_mono {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} {V : set × β)} (f : C(α, β)) {V' : set × β)} (hV' : V' V) :
theorem continuous_map.compact_conv_nhd_mem_comp {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} {V : set × β)} (f : C(α, β)) {g₁ g₂ : C(α, β)} {V' : set × β)} (hg₁ : g₁ continuous_map.compact_conv_nhd K V f) (hg₂ : g₂ continuous_map.compact_conv_nhd K V' g₁) :
theorem continuous_map.compact_conv_nhd_nhd_basis {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} {V : set × β)} (f : C(α, β)) (hV : V uniformity β) :

A key property of compact_conv_nhd. It allows us to apply topological_space.nhds_mk_of_nhds_filter_basis below.

theorem continuous_map.compact_conv_nhd_subset_inter {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (f : C(α, β)) (K₁ K₂ : set α) (V₁ V₂ : set × β)) :
theorem continuous_map.compact_conv_nhd_filter_is_basis {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (f : C(α, β)) :
filter.is_basis (λ (KV : set α × set × β)), is_compact KV.fst KV.snd uniformity β) (λ (KV : set α × set × β)), continuous_map.compact_conv_nhd KV.fst KV.snd f)

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

Equations
theorem continuous_map.mem_compact_convergence_nhd_filter {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (f : C(α, β)) (Y : set C(α, β)) :

The compact-convergence topology. In fact, see compact_open_eq_compact_convergence 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.

Equations
theorem continuous_map.has_basis_nhds_compact_convergence {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (f : C(α, β)) :
(nhds f).has_basis (λ (p : set α × set × β)), is_compact p.fst p.snd uniformity β) (λ (p : set α × set × β)), continuous_map.compact_conv_nhd p.fst p.snd f)
theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on' {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (f : C(α, β)) {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} :
filter.tendsto F p (nhds f) (K : set α), is_compact K tendsto_uniformly_on (λ (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 tendsto_iff_forall_compact_tendsto_uniformly_on below for the useful version where the topology is picked up via typeclass inference.

theorem continuous_map.compact_conv_nhd_subset_compact_open {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} (f : C(α, β)) (hK : is_compact K) {U : set β} (hU : is_open U) (hf : f continuous_map.compact_open.gen K U) :

Any point of compact_open.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 continuous_map.Inter_compact_open_gen_subset_compact_conv_nhd {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {K : set α} {V : set × β)} (f : C(α, β)) (hK : is_compact K) (hV : V uniformity β) :
(ι : Type u₁) [_inst_3 : fintype ι] (C : ι set α) (hC : (i : ι), is_compact (C i)) (U : ι set β) (hU : (i : ι), is_open (U i)), (f (i : ι), continuous_map.compact_open.gen (C i) (U i)) ( (i : ι), continuous_map.compact_open.gen (C i) (U i)) continuous_map.compact_conv_nhd K V f

The point f in compact_conv_nhd K V f is also an interior point wrt the compact-open topology.

Since compact_conv_nhd 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.

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

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

Equations
theorem continuous_map.has_basis_compact_convergence_uniformity_aux {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] :
continuous_map.compact_convergence_uniformity.has_basis (λ (p : set α × set × β)), is_compact p.fst p.snd uniformity β) (λ (p : set α × set × β)), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) p.snd})
theorem continuous_map.mem_compact_convergence_uniformity {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (X : set (C(α, β) × C(α, β))) :
X continuous_map.compact_convergence_uniformity (K : set α) (V : set × β)) (hK : is_compact K) (hV : V uniformity β), {fg : C(α, β) × C(α, β) | (x : α), x K ((fg.fst) x, (fg.snd) x) V} X

An intermediate lemma. Usually mem_compact_convergence_entourage_iff is more useful.

@[protected, instance]

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

Equations
theorem continuous_map.mem_compact_convergence_entourage_iff {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] (X : set (C(α, β) × C(α, β))) :
X uniformity C(α, β) (K : set α) (V : set × β)) (hK : is_compact K) (hV : V uniformity β), {fg : C(α, β) × C(α, β) | (x : α), x K ((fg.fst) x, (fg.snd) x) V} X
theorem continuous_map.has_basis_compact_convergence_uniformity {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] :
(uniformity C(α, β)).has_basis (λ (p : set α × set × β)), is_compact p.fst p.snd uniformity β) (λ (p : set α × set × β)), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) p.snd})
theorem filter.has_basis.compact_convergence_uniformity {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {ι : Type u_1} {pi : ι Prop} {s : ι set × β)} (h : (uniformity β).has_basis pi s) :
(uniformity C(α, β)).has_basis (λ (p : set α × ι), is_compact p.fst pi p.snd) (λ (p : set α × ι), {fg : C(α, β) × C(α, β) | (x : α), x p.fst ((fg.fst) x, (fg.snd) x) s p.snd})
theorem continuous_map.tendsto_iff_forall_compact_tendsto_uniformly_on {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} :
filter.tendsto F p (nhds f) (K : set α), is_compact K tendsto_uniformly_on (λ (i : ι) (a : α), (F i) a) f p K
theorem continuous_map.tendsto_of_tendsto_locally_uniformly {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} (h : tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p) :

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

theorem continuous_map.tendsto_locally_uniformly_of_tendsto {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} (hα : (x : α), (n : set α), is_compact n n nhds x) (h : filter.tendsto F p (nhds f)) :
tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p

If every point has a compact neighbourhood, then convergence in the compact-open topology implies locally uniform convergence.

See also tendsto_iff_tendsto_locally_uniformly, especially for T2 spaces.

theorem continuous_map.tendsto_iff_tendsto_locally_uniformly {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} [locally_compact_space α] :
filter.tendsto F p (nhds f) tendsto_locally_uniformly (λ (i : ι) (a : α), (F i) a) f p

Convergence in the compact-open topology is the same as locally uniform convergence on a locally compact space.

For non-T2 spaces, the assumption locally_compact_space α is stronger than we need and in fact the direction is true unconditionally. See tendsto_locally_uniformly_of_tendsto and tendsto_of_tendsto_locally_uniformly for versions requiring weaker hypotheses.

theorem continuous_map.has_basis_compact_convergence_uniformity_of_compact {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] [compact_space α] :
(uniformity C(α, β)).has_basis (λ (V : set × β)), V uniformity β) (λ (V : set × β)), {fg : C(α, β) × C(α, β) | (x : α), ((fg.fst) x, (fg.snd) x) V})
theorem continuous_map.tendsto_iff_tendsto_uniformly {α : Type u₁} {β : Type u₂} [topological_space α] [uniform_space β] {f : C(α, β)} {ι : Type u₃} {p : filter ι} {F : ι C(α, β)} [compact_space α] :
filter.tendsto F p (nhds f) tendsto_uniformly (λ (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.