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(α, β)
:
- Given a sequence of continuous functions
Fₙ : α → β
together with some continuousf : α → β
, thenFₙ
converges tof
as a sequence inC(α, β)
iffFₙ
converges tof
uniformly on each compact subsetK
ofα
. - Given
Fₙ
andf
as above and supposeα
is locally compact, thenFₙ
converges tof
iffFₙ
converges tof
locally uniformly. - 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 onC(α, β)
iff there exists a compactK
and entourageV
such thatE(K, V) ⊆ X
. - A subset
Y ⊆ C(α, β)
is a neighbourhood off
iff there exists a compactK
and entourageV
such thatN(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 onC(α, β)
.ContinuousMap.mem_compactConvergence_entourage_iff
: a characterisation of the entourages ofC(α, β)
.ContinuousMap.tendsto_iff_forall_compact_tendstoUniformlyOn
: a sequence of functionsFₙ
inC(α, β)
converges to somef
iffFₙ
converges tof
uniformly on each compact subsetK
ofα
.ContinuousMap.tendsto_iff_tendstoLocallyUniformly
: on a locally compact space, a sequence of functionsFₙ
inC(α, β)
converges to somef
iffFₙ
converges tof
locally uniformly.ContinuousMap.tendsto_iff_tendstoUniformly
: on a compact space, a sequence of functionsFₙ
inC(α, β)
converges to somef
iffFₙ
converges tof
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(α, β)
.
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
A key property of ContinuousMap.compactConvNhd
. It allows us to apply
TopologicalSpace.nhds_mkOfNhds_filterBasis
below.
A filter basis for the neighbourhood filter of a point in the compact-convergence topology.
Instances For
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
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.
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.
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.
The compact-open topology is equal to the compact-convergence topology.
The filter on C(α, β) × C(α, β)
which underlies the uniform space structure on C(α, β)
.
Instances For
An intermediate lemma. Usually ContinuousMap.mem_compactConvergence_entourage_iff
is more
useful.
Note that we ensure the induced topology is definitionally the compact-open topology.
Locally uniform convergence implies convergence in the compact-open topology.
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
.
Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space.