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 ofC(α, β)
into the spaceα →ᵤ[{K | IsCompact K}] β
of all mapsα → β
with the uniform space structure of uniform convergence on compacts.ContinuousMap.compactConvergenceUniformSpace
: theUniformSpace
structure onC(α, β)
induced by the map above.
Main results #
ContinuousMap.mem_compactConvergence_entourage_iff
: a characterisation of the entourages ofC(α, β)
.The entourages are generated by the following sets. Given
K : Set α
andV : Set (β × β)
, letE(K, V) : Set (C(α, β) × C(α, β))
be the set of pairs of continuous functionsα → β
which areV
-close onK
: $$ E(K, V) = \{ (f, g) | ∀ (x ∈ K), (f x, g x) ∈ V \}. $$ Then the setsE(K, V)
for all compact setsK
and all entouragesV
form a basis of entourages ofC(α, β)
.As usual, this basis of entourages provides a basis of neighbourhoods by fixing
f
, seenhds_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 functionsFₙ
inC(α, β)
converges in the compact-open topology to somef
iffFₙ
converges tof
uniformly on each compact subsetK
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
toTopologicalSpace
to beContinuousMap.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 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 #
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(α, β)
.
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.
Interpret a bundled continuous map as an element of α →ᵤ[{K | IsCompact K}] β
.
We use this map to induce the UniformSpace
structure on C(α, β)
.
Equations
- f.toUniformOnFunIsCompact = (UniformOnFun.ofFun {K : Set α | IsCompact K}) ⇑f
Instances For
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 ⋯
Alias of ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact
.
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(α, β)
.
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
- ⋯ = ⋯
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
.
Alias of ContinuousMap.isUniformEmbedding_comp
.
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
Convergence in the compact-open topology is the same as uniform convergence for sequences of continuous functions on a compact space.
If the topology on α
is generated by its restrictions to compact sets, then the space of
continuous maps C(α, β)
is complete (wrt the compact convergence uniformity).
Sufficient conditions on α
to satisfy this condition are (weak) local compactness (see
ContinuousMap.instCompleteSpaceOfWeaklyLocallyCompactSpace
) and sequential compactness (see
ContinuousMap.instCompleteSpaceOfSequentialSpace
).
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯