feat(topology/uniform_space): properties of uniform convergence (#9958)

* From the sphere eversion project
* multiple proofs were golfed by @PatrickMassot 
* Probably some proofs can be golfed quite heavily

Co-authored by: Patrick Massot <patrickmassot@free.fr>



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/logic/basic.lean

@@ -816,6 +816,11 @@ exists_congr (λ a, exists₃_congr (h a))
 theorem forall_swap {p : α → β → Prop} : (∀ x y, p x y) ↔ ∀ y x, p x y :=
 ⟨swap, swap⟩
 
+/-- We intentionally restrict the type of `α` in this lemma so that this is a safer to use in simp
+than `forall_swap`. -/
+lemma imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x, q x) ↔ (∀ x, p → q x) :=
+forall_swap
+
 theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y :=
 ⟨λ ⟨x, y, h⟩, ⟨y, x, h⟩, λ ⟨y, x, h⟩, ⟨x, y, h⟩⟩
 

src/order/filter/basic.lean

@@ -2448,6 +2448,27 @@ end
     (λ ht'e, absurd ht'e (nonempty_of_mem ht').ne_empty)),
   λ h, prod_mem_prod h.1 h.2⟩
 
+lemma mem_prod_principal {f : filter α} {s : set (α × β)} {t : set β}:
+  s ∈ f ×ᶠ 𝓟 t ↔ {a | ∀ b ∈ t, (a, b) ∈ s} ∈ f :=
+begin
+  rw [← @exists_mem_subset_iff _ f, mem_prod_iff],
+  apply exists_congr, intro u, apply exists_congr, intro u_in,
+  split,
+  { rintros ⟨v, v_in, hv⟩ a a_in b b_in,
+    exact hv (mk_mem_prod a_in $ v_in b_in) },
+  { intro h,
+    refine ⟨t, mem_principal_self t, _⟩,
+    rintros ⟨x, y⟩ ⟨hx, hy⟩,
+    exact h hx y hy }
+end
+
+lemma mem_prod_top {f : filter α} {s : set (α × β)} :
+  s ∈ f ×ᶠ (⊤ : filter β) ↔ {a | ∀ b, (a, b) ∈ s} ∈ f :=
+begin
+  rw [← principal_univ, mem_prod_principal],
+  simp only [mem_univ, forall_true_left]
+end
+
 lemma comap_prod (f : α → β × γ) (b : filter β) (c : filter γ) :
   comap f (b ×ᶠ c) = (comap (prod.fst ∘ f) b) ⊓ (comap (prod.snd ∘ f) c) :=
 by erw [comap_inf, filter.comap_comap, filter.comap_comap]

src/topology/uniform_space/compact_separated.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot
 -/
 import topology.uniform_space.separation
+import topology.uniform_space.uniform_convergence
 /-!
 # Compact separated uniform spaces
 
@@ -226,3 +227,26 @@ is uniformly continuous. -/
 lemma is_compact.uniform_continuous_on_of_continuous [separated_space α] {s : set α} {f : α → β}
   (hs : is_compact s) (hf : continuous_on f s) : uniform_continuous_on f s :=
 hs.uniform_continuous_on_of_continuous' (is_separated_of_separated_space s) hf
+
+/-- A family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is locally compact,
+`β` is compact and separated and `f` is continuous on `U × (univ : set β)` for some separated
+neighborhood `U` of `x`. -/
+lemma continuous_on.tendsto_uniformly [locally_compact_space α] [compact_space β]
+  [separated_space β] [uniform_space γ] {f : α → β → γ} {x : α} {U : set α}
+  (hxU : U ∈ 𝓝 x) (hU : is_separated U) (h : continuous_on ↿f (U.prod univ)) :
+  tendsto_uniformly f (f x) (𝓝 x) :=
+begin
+  rcases locally_compact_space.local_compact_nhds _ _ hxU with ⟨K, hxK, hKU, hK⟩,
+  have : uniform_continuous_on ↿f (K.prod univ),
+  { refine is_compact.uniform_continuous_on_of_continuous' (hK.prod compact_univ) _
+      (h.mono $ prod_mono hKU subset.rfl),
+    exact (hU.mono hKU).prod (is_separated_of_separated_space _) },
+  exact this.tendsto_uniformly hxK
+end
+
+/-- A continuous family of functions `α → β → γ` tends uniformly to its value at `x` if `α` is
+locally compact and `β` is compact and separated. -/
+lemma continuous.tendsto_uniformly [separated_space α] [locally_compact_space α]
+  [compact_space β] [separated_space β] [uniform_space γ]
+  (f : α → β → γ) (h : continuous ↿f) (x : α) : tendsto_uniformly f (f x) (𝓝 x) :=
+h.continuous_on.tendsto_uniformly univ_mem $ is_separated_of_separated_space _

src/topology/uniform_space/separation.lean

@@ -253,6 +253,8 @@ begin
     exact h ⟨mk_mem_prod x_in y_in, xy_in⟩ }
 end
 
+lemma is_separated.mono {s t : set α} (hs : is_separated s) (hts : t ⊆ s) : is_separated t :=
+λ x y hx hy, hs x y (hts hx) (hts hy)
 
 lemma univ_separated_iff : is_separated (univ : set α) ↔ separated_space α :=
 begin
@@ -264,7 +266,6 @@ begin
     rwa h at xy_in },
 end
 
-
 lemma is_separated_of_separated_space [separated_space α] (s : set α) : is_separated s :=
 begin
   rw [is_separated, separated_space.out],
@@ -435,6 +436,11 @@ lemma eq_of_separated_of_uniform_continuous [separated_space β] {f : α → β}
   (H : uniform_continuous f) (h : x ≈ y) : f x = f y :=
 separated_def.1 (by apply_instance) _ _ $ separated_of_uniform_continuous H h
 
+lemma _root_.is_separated.eq_of_uniform_continuous {f : α → β} {x y : α} {s : set β}
+  (hs : is_separated s) (hxs : f x ∈ s) (hys : f y ∈ s) (H : uniform_continuous f) (h : x ≈ y) :
+  f x = f y :=
+(is_separated_def _).mp hs _ _ hxs hys $ λ _ h', h _ (H h')
+
 /-- The maximal separated quotient of a uniform space `α`. -/
 def separation_quotient (α : Type*) [uniform_space α] := quotient (separation_setoid α)
 
@@ -509,4 +515,11 @@ instance separated.prod [separated_space α] [separated_space β] : separated_sp
 separated_def.2 $ assume x y H, prod.ext
   (eq_of_separated_of_uniform_continuous uniform_continuous_fst H)
   (eq_of_separated_of_uniform_continuous uniform_continuous_snd H)
+
+lemma _root_.is_separated.prod {s : set α} {t : set β} (hs : is_separated s) (ht : is_separated t) :
+  is_separated (s.prod t) :=
+(is_separated_def _).mpr $ assume x y hx hy H, prod.ext
+  (hs.eq_of_uniform_continuous hx.1 hy.1 uniform_continuous_fst H)
+  (ht.eq_of_uniform_continuous hx.2 hy.2 uniform_continuous_snd H)
+
 end uniform_space

src/topology/uniform_space/uniform_convergence.lean

@@ -48,33 +48,55 @@ Uniform limit, uniform convergence, tends uniformly to
  -/
 
 noncomputable theory
-open_locale topological_space classical uniformity
+open_locale topological_space classical uniformity filter
 
 open set filter
 
 universes u v w
-variables {α : Type u} {β : Type v} {γ : Type w}
+variables {α β γ ι : Type*} [uniform_space β]
+variables {F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α}
 
 /-!
 ### Different notions of uniform convergence
 
 We define uniform convergence and locally uniform convergence, on a set or in the whole space.
 -/
 
-variables {ι : Type*} [uniform_space β]
-{F : ι → α → β} {f : α → β} {s s' : set α} {x : α} {p : filter ι} {g : ι → α}
-
 /-- A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with
 respect to the filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
 `(f x, Fₙ x) ∈ u` for all `x ∈ s`. -/
 def tendsto_uniformly_on (F : ι → α → β) (f : α → β) (p : filter ι) (s : set α) :=
-  ∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x ∈ s, (f x, F n x) ∈ u
+∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x ∈ s, (f x, F n x) ∈ u
+
+/--
+A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` w.r.t.
+filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ᶠ 𝓟 s` to the uniformity.
+In other words: one knows nothing about the behavior of `x` in this limit besides it being in `s`.
+-/
+lemma tendsto_uniformly_on_iff_tendsto {F : ι → α → β} {f : α → β} {p : filter ι} {s : set α} :
+  tendsto_uniformly_on F f p s ↔ tendsto (λ q : ι × α, (f q.2, F q.1 q.2)) (p ×ᶠ 𝓟 s) (𝓤 β) :=
+begin
+  refine forall_congr (λ u, forall_congr $ λ u_in, _),
+  simp [mem_map, filter.eventually, mem_prod_principal]
+end
 
 /-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` with respect to a
 filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
 `(f x, Fₙ x) ∈ u` for all `x`. -/
 def tendsto_uniformly (F : ι → α → β) (f : α → β) (p : filter ι) :=
-  ∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x, (f x, F n x) ∈ u
+∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x, (f x, F n x) ∈ u
+
+/--
+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.
+In other words: one knows nothing about the behavior of `x` in this limit.
+-/
+lemma tendsto_uniformly_iff_tendsto {F : ι → α → β} {f : α → β} {p : filter ι} :
+  tendsto_uniformly F f p ↔ tendsto (λ q : ι × α, (f q.2, F q.1 q.2)) (p ×ᶠ ⊤) (𝓤 β) :=
+begin
+  refine forall_congr (λ u, forall_congr $ λ u_in, _),
+  simp [mem_map, filter.eventually, mem_prod_top]
+end
 
 lemma tendsto_uniformly_on_univ :
   tendsto_uniformly_on F f p univ ↔ tendsto_uniformly F f p :=
@@ -106,6 +128,41 @@ begin
   exact λ x, hn _
 end
 
+/-- Uniform convergence to a constant function is equivalent to convergence in `p ×ᶠ ⊤`. -/
+lemma tendsto_prod_top_iff {c : β} : tendsto ↿F (p ×ᶠ ⊤) (𝓝 c) ↔ tendsto_uniformly F (λ _, c) p :=
+let j : β → β × β := prod.mk c in
+calc tendsto ↿F (p ×ᶠ ⊤) (𝓝 c)
+    ↔ map ↿F (p ×ᶠ ⊤) ≤ (𝓝 c) : iff.rfl
+... ↔ map ↿F (p ×ᶠ ⊤) ≤ comap j (𝓤 β) : by rw nhds_eq_comap_uniformity
+... ↔ map j (map ↿F (p ×ᶠ ⊤)) ≤ 𝓤 β : map_le_iff_le_comap.symm
+... ↔ map (j ∘ ↿F) (p ×ᶠ ⊤) ≤ 𝓤 β : by rw map_map
+... ↔ ∀ V ∈ 𝓤 β, {x | (c, ↿F x) ∈ V} ∈ p ×ᶠ (⊤ : filter α) : iff.rfl
+... ↔ ∀ V ∈ 𝓤 β, {i | ∀ a, (c, F i a) ∈ V} ∈ p : by simpa [mem_prod_top]
+
+lemma uniform_continuous_on.tendsto_uniformly [uniform_space α] [uniform_space γ]
+  {x : α} {U : set α} (hU : U ∈ 𝓝 x)
+  {F : α → β → γ} (hF : uniform_continuous_on ↿F (U.prod univ)) :
+  tendsto_uniformly F (F x) (𝓝 x) :=
+begin
+  let φ := (λ q : α × β, ((x, q.2), q)),
+  rw [tendsto_uniformly_iff_tendsto,
+      show (λ q : α × β, (F x q.2, F q.1 q.2)) = prod.map ↿F ↿F ∘ φ, by { ext ; simpa }],
+  apply hF.comp (tendsto_inf.mpr ⟨_, _⟩),
+  { rw [uniformity_prod, tendsto_inf, tendsto_comap_iff, tendsto_comap_iff,
+      show (λp : (α × β) × α × β, (p.1.1, p.2.1)) ∘ φ = (λa, (x, a)) ∘ prod.fst, by { ext, simp },
+      show (λp : (α × β) × α × β, (p.1.2, p.2.2)) ∘ φ = (λb, (b, b)) ∘ prod.snd, by { ext, simp }],
+    exact ⟨tendsto_left_nhds_uniformity.comp tendsto_fst,
+           (tendsto_diag_uniformity id ⊤).comp tendsto_top⟩ },
+  { rw tendsto_principal,
+    apply mem_of_superset (prod_mem_prod hU (mem_top.mpr rfl)) (λ q h, _),
+    simp [h.1, mem_of_mem_nhds hU] }
+end
+
+lemma uniform_continuous₂.tendsto_uniformly [uniform_space α] [uniform_space γ]
+  {f : α → β → γ} (h : uniform_continuous₂ f) {x : α} : tendsto_uniformly f (f x) (𝓝 x) :=
+uniform_continuous_on.tendsto_uniformly univ_mem $
+  by rwa [univ_prod_univ, uniform_continuous_on_univ]
+
 variable [topological_space α]
 
 /-- A sequence of functions `Fₙ` converges locally uniformly on a set `s` to a limiting function