feat(topology/bounded_continuous_functions): more general uniform convergence (#2165)

* feat(topology/buonded_continuous_functions): more general uniform convergence

* yury's comments

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: sgouezel

src/topology/bounded_continuous_function.lean

@@ -18,33 +18,83 @@ open set lattice filter metric
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-/-- A locally uniform limit of continuous functions is continuous -/
-lemma continuous_of_locally_uniform_limit_of_continuous [topological_space α] [metric_space β]
-  {F : ℕ → α → β} {f : α → β}
-  (L : ∀x:α, ∃s ∈ 𝓝 x, ∀ε>(0:ℝ), ∃n, ∀y∈s, dist (F n y) (f y) ≤ ε)
-  (C : ∀ n, continuous (F n)) : continuous f :=
-continuous_iff'.2 $ λ x ε ε0, begin
-  rcases L x with ⟨r, rx, hr⟩,
-  rcases hr (ε/2/2) (half_pos $ half_pos ε0) with ⟨n, hn⟩,
-  filter_upwards [rx, continuous_iff'.1 (C n) x (ε/2) (half_pos ε0)],
+section uniform_limit
+/-!
+### Continuity of uniform limits
+
+In this section, we discuss variations around the continuity of a uniform limit of continuous
+functions when the target space is a metric space. Specifically, we provide statements giving the
+continuity within a set at a point, the continuity at a point, the continuity on a set, and the
+continuity, assuming either locally uniform convergence or globally uniform convergence when this
+makes sense.
+-/
+
+variables {ι : Type*} [topological_space α] [metric_space β]
+{F : ι → α → β} {f : α → β} {s : set α} {x : α}
+
+/-- A locally uniform limit of continuous functions within a set at a point is continuous
+within this set at this point -/
+lemma continuous_within_at_of_locally_uniform_limit_of_continuous_within_at
+  (hx : x ∈ s) (L : ∃t ∈ nhds_within x s, ∀ε>(0:ℝ), ∃n, ∀y∈t, dist (F n y) (f y) ≤ ε)
+  (C : ∀ n, continuous_within_at (F n) s x) : continuous_within_at f s x :=
+begin
+  apply metric.continuous_within_at_iff'.2 (λ ε εpos, _),
+  rcases L with ⟨r, rx, hr⟩,
+  rcases hr (ε/2/2) (half_pos $ half_pos εpos) with ⟨n, hn⟩,
+  filter_upwards [rx, metric.continuous_within_at_iff'.1 (C n) (ε/2) (half_pos εpos)],
   simp only [mem_set_of_eq],
   rintro y yr ys,
   calc dist (f y) (f x)
         ≤ dist (F n y) (F n x) + (dist (F n y) (f y) + dist (F n x) (f x)) : dist_triangle4_left _ _ _ _
     ... < ε/2 + (ε/2/2 + ε/2/2) :
-      add_lt_add_of_lt_of_le ys (add_le_add (hn _ yr) (hn _ (mem_of_nhds rx)))
+      add_lt_add_of_lt_of_le ys (add_le_add (hn _ yr) (hn _ (mem_of_mem_nhds_within hx rx)))
     ... = ε : by rw [add_halves, add_halves]
 end
 
+/-- A locally uniform limit of continuous functions at a point is continuous at this point -/
+lemma continuous_at_of_locally_uniform_limit_of_continuous_at
+  (L : ∃t ∈ 𝓝 x, ∀ε>(0:ℝ), ∃n, ∀y∈t, dist (F n y) (f y) ≤ ε) (C : ∀ n, continuous_at (F n) x) :
+  continuous_at f x :=
+begin
+  simp only [← continuous_within_at_univ] at C ⊢,
+  apply continuous_within_at_of_locally_uniform_limit_of_continuous_within_at (mem_univ _) _ C,
+  simpa [nhds_within_univ] using L
+end
+
+/-- A locally uniform limit of continuous functions on a set is continuous on this set -/
+lemma continuous_on_of_locally_uniform_limit_of_continuous_on
+  (L : ∀ (x ∈ s), ∃t ∈ nhds_within x s, ∀ε>(0:ℝ), ∃n, ∀y∈t, dist (F n y) (f y) ≤ ε)
+  (C : ∀ n, continuous_on (F n) s) : continuous_on f s :=
+λ x hx, continuous_within_at_of_locally_uniform_limit_of_continuous_within_at hx
+  (L x hx) (λ n, C n x hx)
+
+/-- A uniform limit of continuous functions on a set is continuous on this set -/
+lemma continuous_on_of_uniform_limit_of_continuous_on
+  (L : ∀ε>(0:ℝ), ∃N, ∀y ∈ s, dist (F N y) (f y) ≤ ε) :
+  (∀ n, continuous_on (F n) s) → continuous_on f s :=
+continuous_on_of_locally_uniform_limit_of_continuous_on (λ x hx, ⟨s, self_mem_nhds_within, L⟩)
+
+/-- A locally uniform limit of continuous functions is continuous -/
+lemma continuous_of_locally_uniform_limit_of_continuous
+  (L : ∀x:α, ∃s ∈ 𝓝 x, ∀ε>(0:ℝ), ∃n, ∀y∈s, dist (F n y) (f y) ≤ ε)
+  (C : ∀ n, continuous (F n)) : continuous f :=
+begin
+  simp only [continuous_iff_continuous_on_univ] at ⊢ C,
+  apply continuous_on_of_locally_uniform_limit_of_continuous_on _ C,
+  simpa [nhds_within_univ] using L
+end
+
 /-- A uniform limit of continuous functions is continuous -/
-lemma continuous_of_uniform_limit_of_continuous [topological_space α] {β : Type v} [metric_space β]
-  {F : ℕ → α → β} {f : α → β} (L : ∀ε>(0:ℝ), ∃N, ∀y, dist (F N y) (f y) ≤ ε) :
+lemma continuous_of_uniform_limit_of_continuous (L : ∀ε>(0:ℝ), ∃N, ∀y, dist (F N y) (f y) ≤ ε) :
   (∀ n, continuous (F n)) → continuous f :=
 continuous_of_locally_uniform_limit_of_continuous $ λx,
   ⟨univ, by simpa [filter.univ_mem_sets] using L⟩
 
+end uniform_limit
+
 /-- The type of bounded continuous functions from a topological space to a metric space -/
-def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] : Type (max u v) :=
+def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
+  Type (max u v) :=
 {f : α → β // continuous f ∧ ∃C, ∀x y:α, dist (f x) (f y) ≤ C}
 
 local infixr ` →ᵇ `:25 := bounded_continuous_function

src/topology/continuous_on.lean

@@ -219,6 +219,10 @@ lemma continuous_within_at.tendsto {f : α → β} {s : set α} {x : α} (h : co
 when it's continuous at every point of `s` within `s`. -/
 def continuous_on (f : α → β) (s : set α) : Prop := ∀ x ∈ s, continuous_within_at f s x
 
+lemma continuous_on.continuous_within_at {f : α → β} {s : set α} {x : α} (hf : continuous_on f s)
+  (hx : x ∈ s) : continuous_within_at f s x :=
+hf x hx
+
 theorem continuous_within_at_univ (f : α → β) (x : α) :
   continuous_within_at f set.univ x ↔ continuous_at f x :=
 by rw [continuous_at, continuous_within_at, nhds_within_univ]
@@ -260,7 +264,7 @@ have ∀ t, is_open (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_op
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous]; simp only [this]
 
-theorem continuous_on_iff_is_closed  {f : α → β} {s : set α} :
+theorem continuous_on_iff_is_closed {f : α → β} {s : set α} :
   continuous_on f s ↔ ∀ t : set β, is_closed t → ∃ u, is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s :=
 have ∀ t, is_closed (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_closed u ∧ f ⁻¹' t ∩ s = u ∩ s,
   begin
@@ -270,6 +274,9 @@ have ∀ t, is_closed (function.restrict f s ⁻¹' t) ↔ ∃ (u : set α), is_
   end,
 by rw [continuous_on_iff_continuous_restrict, continuous_iff_is_closed]; simp only [this]
 
+lemma continuous_on_empty (f : α → β) : continuous_on f ∅ :=
+λ x, false.elim
+
 theorem nhds_within_le_comap {x : α} {s : set α} {f : α → β} (ctsf : continuous_within_at f s x) :
   nhds_within x s ≤ comap f (nhds_within (f x) (f '' s)) :=
 map_le_iff_le_comap.1 ctsf.tendsto_nhds_within_image
@@ -374,6 +381,10 @@ begin
   rwa [this, continuous_within_at_inter hs, continuous_within_at_univ] at h
 end
 
+lemma continuous_on.continuous_at {f : α → β} {s : set α} {x : α}
+  (h : continuous_on f s) (hx : s ∈ 𝓝 x) : continuous_at f x :=
+(h x (mem_of_nhds hx)).continuous_at hx
+
 lemma continuous_within_at.comp {g : β → γ} {f : α → β} {s : set α} {t : set β} {x : α}
   (hg : continuous_within_at g t (f x)) (hf : continuous_within_at f s x) (h : s ⊆ f ⁻¹' t) :
   continuous_within_at (g ∘ f) s x :=

src/topology/metric_space/basic.lean

@@ -298,6 +298,9 @@ theorem ball_eq_empty_iff_nonpos : ε ≤ 0 ↔ ball x ε = ∅ :=
 ⟨λ h, le_of_not_gt $ λ ε0, h _ $ mem_ball_self ε0,
  λ ε0 y h, not_lt_of_le ε0 $ pos_of_mem_ball h⟩).symm
 
+@[simp] lemma ball_zero : ball x 0 = ∅ :=
+by rw [← metric.ball_eq_empty_iff_nonpos]
+
 theorem uniformity_basis_dist :
   (𝓤 α).has_basis (λ ε : ℝ, 0 < ε) (λ ε, {p:α×α | dist p.1 p.2 < ε}) :=
 (metric_space.uniformity_dist α).symm ▸ has_basis_binfi_principal
@@ -496,15 +499,47 @@ theorem continuous_at_iff [metric_space β] {f : α → β} {a : α} :
     ∀ ε > 0, ∃ δ > 0, ∀{x:α}, dist x a < δ → dist (f x) (f a) < ε :=
 by rw [continuous_at, tendsto_nhds_nhds]
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem continuous_within_at_iff [metric_space β] {f : α → β} {a : α} {s : set α} :
+  continuous_within_at f s a ↔
+  ∀ ε > 0, ∃ δ > 0, ∀{x:α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε :=
+by rw [continuous_within_at, tendsto_nhds_within_nhds]
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem continuous_on_iff [metric_space β] {f : α → β} {s : set α} :
+  continuous_on f s ↔
+  ∀ (b ∈ s) (ε > 0), ∃ δ > 0, ∀a ∈ s, dist a b < δ → dist (f a) (f b) < ε :=
+by simp [continuous_on, continuous_within_at_iff]
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem continuous_iff [metric_space β] {f : α → β} :
   continuous f ↔
-    ∀b (ε > 0), ∃ δ > 0, ∀a, dist a b < δ → dist (f a) (f b) < ε :=
+  ∀b (ε > 0), ∃ δ > 0, ∀a, dist a b < δ → dist (f a) (f b) < ε :=
 continuous_iff_continuous_at.trans $ forall_congr $ λ b, tendsto_nhds_nhds
 
 theorem tendsto_nhds {f : filter β} {u : β → α} {a : α} :
   tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, dist (u x) a < ε :=
 nhds_basis_ball.tendsto_right_iff
 
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem continuous_at_iff' [topological_space β] {f : β → α} {b : β} :
+  continuous_at f b ↔
+  ∀ ε > 0, ∀ᶠ x in 𝓝 b, dist (f x) (f b) < ε :=
+by rw [continuous_at, tendsto_nhds]
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem continuous_within_at_iff' [topological_space β] {f : β → α} {b : β} {s : set β} :
+  continuous_within_at f s b ↔
+  ∀ ε > 0, ∀ᶠ x in nhds_within b s, dist (f x) (f b) < ε :=
+by rw [continuous_within_at, tendsto_nhds]
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem continuous_on_iff' [topological_space β] {f : β → α} {s : set β} :
+  continuous_on f s ↔
+  ∀ (b ∈ s) (ε > 0), ∀ᶠ x in nhds_within b s, dist (f x) (f b) < ε  :=
+by simp [continuous_on, continuous_within_at_iff']
+
+@[nolint ge_or_gt] -- see Note [nolint_ge]
 theorem continuous_iff' [topological_space β] {f : β → α} :
   continuous f ↔ ∀a (ε > 0), ∀ᶠ x in 𝓝 a, dist (f x) (f a) < ε :=
 continuous_iff_continuous_at.trans $ forall_congr $ λ b, tendsto_nhds

src/topology/metric_space/emetric_space.lean

@@ -518,6 +518,9 @@ eq_empty_iff_forall_not_mem.trans
 ⟨λh, le_bot_iff.1 (le_of_not_gt (λ ε0, h _ (mem_ball_self ε0))),
 λε0 y h, not_lt_of_le (le_of_eq ε0) (pos_of_mem_ball h)⟩
 
+@[simp] lemma ball_zero : ball x 0 = ∅ :=
+by rw [emetric.ball_eq_empty_iff]
+
 theorem nhds_basis_eball : (𝓝 x).has_basis (λ ε:ennreal, 0 < ε) (ball x) :=
 nhds_basis_uniformity uniformity_basis_edist