Docs

Mathlib/Topology/UniformSpace/CompactConvergence.lean

@@ -12,70 +12,77 @@ import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
 # 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.
+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 of `C(α, β)`
+  into the space `α →ᵤ[{K | IsCompact K}] β` of all maps `α → β`
+  with the uniform space structure of uniform convergence on compacts.
+
+- `ContinuousMap.compactConvergenceUniformSpace`:
+  the `UniformSpace` structure on `C(α, β)` induced by the map above.
+
+## Main results
+
+* `ContinuousMap.mem_compactConvergence_entourage_iff`:
+  a characterisation of the entourages of `C(α, β)`.
+
+  The entourages are generated by the following sets.
+  Given `K : Set α` and `V : Set (β × β)`,
+  let `E(K, V) : Set (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 \}.
+  $$
+  Then the sets `E(K, V)` for all compact sets `K` and all entourages `V`
+  form a basis of entourages of `C(α, β)`.
+
+  As usual, this basis of entourages provides a basis of neighbourhoods
+  by fixing `f`, see `nhds_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 functions `Fₙ` in `C(α, β)` converges in the compact-open topology to some `f`
+  iff `Fₙ` converges to `f` uniformly on each compact subset `K` 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`
+  to `TopologicalSpace` to be `ContinuousMap.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 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.
+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
 
- * 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(α, β)`.
+* 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(α, β)`.
 -/
 
 
@@ -218,7 +225,6 @@ theorem mem_compactConvergence_entourage_iff (X : Set (C(α, β) × C(α, β)))
 
 variable {ι : Type u₃} {p : Filter ι} {F : ι → C(α, β)} {f}
 
-
 /-- Locally uniform convergence implies convergence in the compact-open topology. -/
 theorem tendsto_of_tendstoLocallyUniformly (h : TendstoLocallyUniformly (fun i a => F i a) f p) :
     Tendsto F p (𝓝 f) := by