feat(topology/uniform_space/compact_convergence): when the domain is …

…locally compact, compact convergence is just locally uniform convergence (#11292)

Also, locally uniform convergence is just uniform convergence when the domain is compact.

src/topology/uniform_space/compact_convergence.lean

@@ -17,10 +17,12 @@ 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. The topology coincides with the compact-open topology.
+ 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 but 2 requires a little work and uses the Lebesgue
-number lemma.
+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
 
@@ -52,6 +54,10 @@ neighbourhood basis (the compact-convergence neighbourhood basis).
  * `mem_compact_convergence_entourage_iff`: a characterisation of the entourages of `C(α, β)`.
  * `tendsto_iff_forall_compact_tendsto_uniformly_on`: a sequence of functions `Fₙ` in `C(α, β)`
    converges to some `f` iff `Fₙ` converges to `f` uniformly on each compact subset `K` of `α`.
+ * `tendsto_iff_tendsto_locally_uniformly`: on a locally compact space, a sequence of functions
+   `Fₙ` in `C(α, β)` converges to some `f` iff `Fₙ` converges to `f` locally uniformly.
+ * `tendsto_iff_tendsto_uniformly`: on a compact space, a sequence of functions `Fₙ` in `C(α, β)`
+   converges to some `f` iff `Fₙ` converges to `f` uniformly.
 
 ## Implementation details
 
@@ -343,11 +349,46 @@ lemma has_basis_compact_convergence_uniformity :
             (λ p, { fg : C(α, β) × C(α, β) | ∀ x ∈ p.1, (fg.1 x, fg.2 x) ∈ p.2 }) :=
 ⟨λ t, by { simp only [mem_compact_convergence_entourage_iff, prod.exists], tauto, }⟩
 
-lemma tendsto_iff_forall_compact_tendsto_uniformly_on
-  {ι : Type u₃} {p : filter ι} {F : ι → C(α, β)} :
-  filter.tendsto F p (𝓝 f) ↔ ∀ K, is_compact K → tendsto_uniformly_on (λ i a, F i a) f p K :=
+variables {ι : Type u₃} {p : filter ι} {F : ι → C(α, β)} {f}
+
+lemma tendsto_iff_forall_compact_tendsto_uniformly_on :
+  tendsto F p (𝓝 f) ↔ ∀ K, is_compact K → tendsto_uniformly_on (λ i a, F i a) f p K :=
 by rw [compact_open_eq_compact_convergence, tendsto_iff_forall_compact_tendsto_uniformly_on']
 
+/-- Locally uniform convergence implies convergence in the compact-open topology. -/
+lemma tendsto_of_tendsto_locally_uniformly
+  (h : tendsto_locally_uniformly (λ i a, F i a) f p) : tendsto F p (𝓝 f) :=
+begin
+  rw tendsto_iff_forall_compact_tendsto_uniformly_on,
+  intros K hK,
+  rw ← tendsto_locally_uniformly_on_iff_tendsto_uniformly_on_of_compact hK,
+  exact h.tendsto_locally_uniformly_on,
+end
+
+/-- 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. -/
+lemma tendsto_locally_uniformly_of_tendsto
+  (hα : ∀ x : α, ∃ n, is_compact n ∧ n ∈ 𝓝 x) (h : tendsto F p (𝓝 f)) :
+  tendsto_locally_uniformly (λ i a, F i a) f p :=
+begin
+  rw tendsto_iff_forall_compact_tendsto_uniformly_on at h,
+  intros V hV x,
+  obtain ⟨n, hn₁, hn₂⟩ := hα x,
+  exact ⟨n, hn₂, h n hn₁ V hV⟩,
+end
+
+/-- 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. -/
+lemma tendsto_iff_tendsto_locally_uniformly [locally_compact_space α] :
+  tendsto F p (𝓝 f) ↔ tendsto_locally_uniformly (λ i a, F i a) f p :=
+⟨tendsto_locally_uniformly_of_tendsto exists_compact_mem_nhds, tendsto_of_tendsto_locally_uniformly⟩
+
 section compact_domain
 
 variables [compact_space α]
@@ -361,9 +402,8 @@ has_basis_compact_convergence_uniformity.to_has_basis
 
 /-- Convergence in the compact-open topology is the same as uniform convergence for sequences of
 continuous functions on a compact space. -/
-lemma tendsto_iff_tendsto_uniformly
-  {ι : Type u₃} {p : filter ι} {F : ι → C(α, β)} :
-  filter.tendsto F p (𝓝 f) ↔ tendsto_uniformly (λ i a, F i a) f p :=
+lemma tendsto_iff_tendsto_uniformly :
+  tendsto F p (𝓝 f) ↔ tendsto_uniformly (λ i a, F i a) f p :=
 begin
   rw [tendsto_iff_forall_compact_tendsto_uniformly_on, ← tendsto_uniformly_on_univ],
   exact ⟨λ h, h univ compact_univ, λ h K hK, h.mono (subset_univ K)⟩,

src/topology/uniform_space/uniform_convergence.lean

@@ -86,6 +86,11 @@ filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
 def tendsto_uniformly (F : ι → α → β) (f : α → β) (p : filter ι) :=
 ∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x, (f x, F n x) ∈ u
 
+lemma tendsto_uniformly_on_iff_tendsto_uniformly_comp_coe :
+  tendsto_uniformly_on F f p s ↔
+  tendsto_uniformly (λ i (x : s), F i x) (f ∘ coe) p :=
+forall_congr (λ V, forall_congr (λ hV, by simp))
+
 /--
 A sequence of functions `Fₙ` converges uniformly to a limiting function `f` w.r.t.
 filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ᶠ ⊤` to the uniformity.
@@ -167,16 +172,35 @@ variable [topological_space α]
 
 /-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function
 `f` with respect to a filter `p` if, for any entourage of the diagonal `u`, for any `x ∈ s`, one
-has `p`-eventually `(f x, Fₙ x) ∈ u` for all `y` in a neighborhood of `x` in `s`. -/
+has `p`-eventually `(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x` in `s`. -/
 def tendsto_locally_uniformly_on (F : ι → α → β) (f : α → β) (p : filter ι) (s : set α) :=
   ∀ u ∈ 𝓤 β, ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u
 
 /-- A sequence of functions `Fₙ` converges locally uniformly to a limiting function `f` with respect
 to a filter `p` if, for any entourage of the diagonal `u`, for any `x`, one has `p`-eventually
-`(f x, Fₙ x) ∈ u` for all `y` in a neighborhood of `x`. -/
+`(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x`. -/
 def tendsto_locally_uniformly (F : ι → α → β) (f : α → β) (p : filter ι) :=
   ∀ u ∈ 𝓤 β, ∀ (x : α), ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u
 
+lemma tendsto_locally_uniformly_on_iff_tendsto_locally_uniformly_comp_coe :
+  tendsto_locally_uniformly_on F f p s ↔
+  tendsto_locally_uniformly (λ i (x : s), F i x) (f ∘ coe) p :=
+begin
+  refine forall_congr (λ V, forall_congr (λ hV, _)),
+  simp only [exists_prop, function.comp_app, set_coe.forall, subtype.coe_mk],
+  refine forall_congr (λ x, forall_congr (λ hx, ⟨λ h, _, λ h, _⟩)),
+  { obtain ⟨t, ht₁, ht₂⟩ := h,
+    obtain ⟨u, hu₁, hu₂⟩ := mem_nhds_within_iff_exists_mem_nhds_inter.mp ht₁,
+    exact ⟨coe⁻¹' u,
+           (mem_nhds_subtype _ _ _).mpr ⟨u, hu₁, rfl.subset⟩,
+           ht₂.mono (λ i hi y hy₁ hy₂, hi y (hu₂ ⟨hy₂, hy₁⟩))⟩, },
+  { obtain ⟨t, ht₁, ht₂⟩ := h,
+    obtain ⟨u, hu₁, hu₂⟩ := (mem_nhds_subtype _ _ _).mp ht₁,
+    exact ⟨u ∩ s,
+           mem_nhds_within_iff_exists_mem_nhds_inter.mpr ⟨u, hu₁, rfl.subset⟩,
+           ht₂.mono (λ i hi y hy, hi y hy.2 (hu₂ (by simp [hy.1])))⟩, },
+end
+
 protected lemma tendsto_uniformly_on.tendsto_locally_uniformly_on
   (h : tendsto_uniformly_on F f p s) : tendsto_locally_uniformly_on F f p s :=
 λ u hu x hx, ⟨s, self_mem_nhds_within, h u hu⟩
@@ -201,6 +225,33 @@ protected lemma tendsto_locally_uniformly.tendsto_locally_uniformly_on
   (h : tendsto_locally_uniformly F f p) : tendsto_locally_uniformly_on F f p s :=
 (tendsto_locally_uniformly_on_univ.mpr h).mono (subset_univ _)
 
+/-- On a compact space, locally uniform convergence is just uniform convergence. -/
+lemma tendsto_locally_uniformly_iff_tendsto_uniformly_of_compact_space [compact_space α] :
+  tendsto_locally_uniformly F f p ↔ tendsto_uniformly F f p :=
+begin
+  refine ⟨λ h V hV, _, tendsto_uniformly.tendsto_locally_uniformly⟩,
+  choose U hU using h V hV,
+  obtain ⟨t, ht⟩ := compact_univ.elim_nhds_subcover' (λ k hk, U k) (λ k hk, (hU k).1),
+  replace hU := λ (x : t), (hU x).2,
+  rw ← eventually_all at hU,
+  refine hU.mono (λ i hi x, _),
+  specialize ht (mem_univ x),
+  simp only [exists_prop, mem_Union, set_coe.exists, exists_and_distrib_right,subtype.coe_mk] at ht,
+  obtain ⟨y, ⟨hy₁, hy₂⟩, hy₃⟩ := ht,
+  exact hi ⟨⟨y, hy₁⟩, hy₂⟩ x hy₃,
+end
+
+/-- For a compact set `s`, locally uniform convergence on `s` is just uniform convergence on `s`. -/
+lemma tendsto_locally_uniformly_on_iff_tendsto_uniformly_on_of_compact (hs : is_compact s) :
+  tendsto_locally_uniformly_on F f p s ↔ tendsto_uniformly_on F f p s :=
+begin
+  haveI : compact_space s := is_compact_iff_compact_space.mp hs,
+  refine ⟨λ h, _, tendsto_uniformly_on.tendsto_locally_uniformly_on⟩,
+  rwa [tendsto_locally_uniformly_on_iff_tendsto_locally_uniformly_comp_coe,
+    tendsto_locally_uniformly_iff_tendsto_uniformly_of_compact_space,
+    ← tendsto_uniformly_on_iff_tendsto_uniformly_comp_coe] at h,
+end
+
 lemma tendsto_locally_uniformly_on.comp [topological_space γ] {t : set γ}
   (h : tendsto_locally_uniformly_on F f p s)
   (g : γ → α) (hg : maps_to g t s) (cg : continuous_on g t) :