feat(topology/bounded_continuous_function): composition of limits whe…

…n uniform convergence (#2260)

* feat(topology/bounded_continuous_function): composition of limits when uniform convergence

* better statement

* uniform space version

* cleanup

* fix linter

* reviewer's comments

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

src/analysis/analytic/basic.lean

@@ -309,7 +309,7 @@ let ⟨rf, hrf⟩ := hf in hrf.coeff_zero v
 
 /-- If a function admits a power series expansion, then it is exponentially close to the partial
 sums of this power series on strict subdisks of the disk of convergence. -/
-lemma has_fpower_series_on_ball.uniform_limit {r' : nnreal}
+lemma has_fpower_series_on_ball.uniform_geometric_approx {r' : nnreal}
   (hf : has_fpower_series_on_ball f p x r) (h : (r' : ennreal) < r) :
   ∃ (a C : nnreal), a < 1 ∧ (∀ y ∈ metric.ball (0 : E) r', ∀ n,
   ∥f (x + y) - p.partial_sum n y∥ ≤ C * a ^ n) :=
@@ -336,38 +336,72 @@ begin
     ... ≤ C * a ^ n : by exact_mod_cast hC n,
 end
 
+/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
+partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f (x + y)`
+is the uniform limit of `p.partial_sum n y` there. -/
+lemma has_fpower_series_on_ball.tendsto_uniformly_on {r' : nnreal}
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ennreal) < r) :
+  tendsto_uniformly_on (λ n y, p.partial_sum n y) (λ y, f (x + y)) at_top (metric.ball (0 : E) r') :=
+begin
+  rcases hf.uniform_geometric_approx h with ⟨a, C, ha, hC⟩,
+  refine metric.tendsto_uniformly_on_iff.2 (λ ε εpos, _),
+  have L : tendsto (λ n, (C : ℝ) * a^n) at_top (𝓝 ((C : ℝ) * 0)) :=
+    tendsto_const_nhds.mul (tendsto_pow_at_top_nhds_0_of_lt_1 (a.2) ha),
+  rw mul_zero at L,
+  apply ((tendsto_order.1 L).2 ε εpos).mono (λ n hn, _),
+  assume y hy,
+  rw dist_eq_norm,
+  exact lt_of_le_of_lt (hC y hy n) hn
+end
+
+/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
+the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
+is the locally uniform limit of `p.partial_sum n y` there. -/
+lemma has_fpower_series_on_ball.tendsto_locally_uniformly_on
+  (hf : has_fpower_series_on_ball f p x r) :
+  tendsto_locally_uniformly_on (λ n y, p.partial_sum n y) (λ y, f (x + y))
+  at_top (emetric.ball (0 : E) r) :=
+begin
+  assume u hu x hx,
+  rcases ennreal.lt_iff_exists_nnreal_btwn.1 hx with ⟨r', xr', hr'⟩,
+  have : emetric.ball (0 : E) r' ∈ 𝓝 x :=
+    mem_nhds_sets emetric.is_open_ball xr',
+  refine ⟨emetric.ball (0 : E) r', mem_nhds_within_of_mem_nhds this, _⟩,
+  simpa [metric.emetric_ball_nnreal] using hf.tendsto_uniformly_on hr' u hu
+end
+
+/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
+partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f y`
+is the uniform limit of `p.partial_sum n (y - x)` there. -/
+lemma has_fpower_series_on_ball.tendsto_uniformly_on' {r' : nnreal}
+  (hf : has_fpower_series_on_ball f p x r) (h : (r' : ennreal) < r) :
+  tendsto_uniformly_on (λ n y, p.partial_sum n (y - x)) f at_top (metric.ball (x : E) r') :=
+begin
+  convert (hf.tendsto_uniformly_on h).comp (λ y, y - x),
+  { ext z, simp },
+  { ext z, simp [dist_eq_norm] }
+end
+
+/-- If a function admits a power series expansion at `x`, then it is the locally uniform limit of
+the  partial sums of this power series on the disk of convergence, i.e., `f y`
+is the locally uniform limit of `p.partial_sum n (y - x)` there. -/
+lemma has_fpower_series_on_ball.tendsto_locally_uniformly_on'
+  (hf : has_fpower_series_on_ball f p x r) :
+  tendsto_locally_uniformly_on (λ n y, p.partial_sum n (y - x)) f at_top (emetric.ball (x : E) r) :=
+begin
+  have A : continuous_on (λ (y : E), y - x) (emetric.ball (x : E) r) :=
+    (continuous_id.sub continuous_const).continuous_on,
+  convert (hf.tendsto_locally_uniformly_on).comp (λ (y : E), y - x) _ A,
+  { ext z, simp },
+  { assume z, simp [edist_eq_coe_nnnorm, edist_eq_coe_nnnorm_sub] }
+end
+
 /-- If a function admits a power series expansion on a disk, then it is continuous there. -/
 lemma has_fpower_series_on_ball.continuous_on
   (hf : has_fpower_series_on_ball f p x r) : continuous_on f (emetric.ball x r) :=
 begin
-  have : ∀ n, continuous_on (λ y, p.partial_sum n (y - x)) (emetric.ball x r) :=
-    λ n, ((p.partial_sum_continuous n).comp (continuous_id.sub continuous_const)).continuous_on,
-  apply continuous_on_of_locally_uniform_limit_of_continuous_on (λ y hy, _) this,
-  have : (nnnorm (y - x) : ennreal) < r,
-    by { rw ← edist_eq_coe_nnnorm_sub, exact hy },
-  rcases ennreal.lt_iff_exists_nnreal_btwn.1 this with ⟨r', xr', r'r⟩,
-  rw ennreal.coe_lt_coe at xr',
-  refine ⟨metric.ball x r', _, λ ε εpos, _⟩,
-  show metric.ball x r' ∈ nhds_within y (emetric.ball x r),
-  { apply mem_nhds_within_of_mem_nhds,
-    apply mem_nhds_sets metric.is_open_ball,
-    change dist y x < r',
-    rwa [dist_nndist, nnreal.coe_lt_coe, nndist_eq_nnnorm] },
-  show ∃ (n : ℕ),
-    ∀ z ∈ metric.ball x ↑r', dist (formal_multilinear_series.partial_sum p n (z - x)) (f z) ≤ ε,
-  { obtain ⟨a, C, ha, hC⟩ : ∃ (a C : nnreal), a < 1 ∧ (∀ y ∈ metric.ball (0 : E) r', ∀ n,
-      ∥f (x + y) - p.partial_sum n y∥ ≤ C * a ^ n) := hf.uniform_limit r'r,
-    have L : tendsto (λ (n : ℕ), (C : ℝ) * a ^ n) at_top (𝓝 ((C : ℝ) * 0)) :=
-      tendsto_const_nhds.mul (tendsto_pow_at_top_nhds_0_of_lt_1 (a.2) ha),
-    rw mul_zero at L,
-    obtain ⟨n, hn⟩ : ∃ (n : ℕ), (C : ℝ) * a ^ n < ε :=
-      eventually.exists ((tendsto_order.1 L).2 _ εpos) at_top_ne_bot,
-    refine ⟨n, λ z hz, _⟩,
-    have : z - x ∈ metric.ball (0 : E) r',
-      by { rwa [metric.mem_ball, dist_eq_norm, ← dist_zero_right] at hz },
-    rw [dist_eq_norm, norm_sub_rev],
-    convert le_trans (hC _ this n) (le_of_lt hn),
-    abel }
+  apply hf.tendsto_locally_uniformly_on'.continuous_on _ at_top_ne_bot,
+  exact λ n, ((p.partial_sum_continuous n).comp (continuous_id.sub continuous_const)).continuous_on
 end
 
 lemma has_fpower_series_at.continuous_at (hf : has_fpower_series_at f p x) : continuous_at f x :=

src/data/real/nnreal.lean

@@ -19,6 +19,9 @@ namespace nnreal
 
 instance : has_coe ℝ≥0 ℝ := ⟨subtype.val⟩
 
+/- Simp lemma to put back `n.val` into the normal form given by the coercion. -/
+@[simp] lemma val_eq_coe (n : nnreal) : n.val = n := rfl
+
 instance : can_lift ℝ nnreal :=
 { coe := coe,
   cond := λ r, r ≥ 0,

src/topology/basic.lean

@@ -429,6 +429,10 @@ attribute [irreducible] nhds
 lemma mem_of_nhds {a : α} {s : set α} : s ∈ 𝓝 a → a ∈ s :=
 λ H, let ⟨t, ht, _, hs⟩ := mem_nhds_sets_iff.1 H in ht hs
 
+lemma filter.eventually.self_of_nhds {p : α → Prop} {a : α}
+  (h : ∀ᶠ y in 𝓝 a, p y) : p a :=
+mem_of_nhds h
+
 lemma mem_nhds_sets {a : α} {s : set α} (hs : is_open s) (ha : a ∈ s) :
  s ∈ 𝓝 a :=
 mem_nhds_sets_iff.2 ⟨s, subset.refl _, hs, ha⟩

src/topology/bounded_continuous_function.lean

@@ -2,96 +2,26 @@
 Copyright (c) 2018 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel, Mario Carneiro
+-/
+
+import analysis.normed_space.basic topology.metric_space.lipschitz
 
-Type of bounded continuous functions taking values in a metric space, with
+/-!
+# Bounded continuous functions
+
+The type of bounded continuous functions taking values in a metric space, with
 the uniform distance.
- -/
 
-import analysis.normed_space.basic topology.metric_space.lipschitz
+-/
 
 noncomputable theory
-local attribute [instance] classical.decidable_inhabited classical.prop_decidable
-open_locale topological_space
+open_locale topological_space classical
 
 open set filter metric
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-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_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 (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) :=
@@ -213,13 +143,13 @@ begin
       (tendsto_const_nhds.dist (hF x))
       (filter.eventually_at_top.2 ⟨N, λn hn, f_bdd x N n N (le_refl N) hn⟩),
   refine ⟨⟨F, _, _⟩, _⟩,
-  { /- Check that `F` is continuous -/
-    refine continuous_of_uniform_limit_of_continuous (λ ε ε0, _) (λN, (f N).2.1),
-    rcases metric.tendsto_at_top.1 b_lim ε ε0 with ⟨N, hN⟩,
-    exact ⟨N, λy, calc
-      dist (f N y) (F y) ≤ b N : fF_bdd y N
-      ... ≤ dist (b N) 0 : begin simp, show b N ≤ abs(b N), from le_abs_self _ end
-      ... ≤ ε : le_of_lt (hN N (le_refl N))⟩ },
+  { /- Check that `F` is continuous, as a uniform limit of continuous functions -/
+    have : tendsto_uniformly (λn x, f n x) F at_top,
+    { refine metric.tendsto_uniformly_iff.2 (λ ε ε0, _),
+      refine ((tendsto_order.1 b_lim).2 ε ε0).mono (λ n hn x, _),
+      rw dist_comm,
+      exact lt_of_le_of_lt (fF_bdd x n) hn },
+    exact this.continuous (λN, (f N).2.1) at_top_ne_bot },
   { /- Check that `F` is bounded -/
     rcases (f 0).2.2 with ⟨C, hC⟩,
     exact ⟨C + (b 0 + b 0), λ x y, calc

src/topology/continuous_on.lean

@@ -76,6 +76,10 @@ lemma mem_of_mem_nhds_within {a : α} {s t : set α} (ha : a ∈ s) (ht : t ∈
   a ∈ t :=
 let ⟨u, hu, H⟩ := mem_nhds_within.1 ht in H.2 ⟨H.1, ha⟩
 
+lemma filter.eventually.self_of_nhds_within {p : α → Prop} {s : set α} {x : α}
+  (h : ∀ᶠ y in nhds_within x s, p y) (hx : x ∈ s) : p x :=
+mem_of_mem_nhds_within hx h
+
 theorem nhds_within_restrict'' {a : α} (s : set α) {t : set α} (h : t ∈ nhds_within a s) :
   nhds_within a s = nhds_within a (s ∩ t) :=
 le_antisymm

src/topology/metric_space/basic.lean

@@ -10,11 +10,11 @@ topological spaces. For example:
   open and closed sets, compactness, completeness, continuity and uniform continuity
 -/
 import data.real.nnreal topology.metric_space.emetric_space topology.algebra.ordered
+
 open set filter classical topological_space
 noncomputable theory
 
-open_locale uniformity
-open_locale topological_space
+open_locale uniformity topological_space
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -435,6 +435,45 @@ begin
   exact ⟨_, ⟨F ⟨x, xs⟩, rfl⟩, hF _ _ this.symm⟩
 end
 
+/-- Expressing locally uniform convergence on a set using `dist`. -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma tendsto_locally_uniformly_on_iff {ι : Type*} [topological_space β]
+  {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
+  tendsto_locally_uniformly_on F f p s ↔
+  ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhds_within x s, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε :=
+begin
+  refine ⟨λ H ε hε, H _ (dist_mem_uniformity hε), λ H u hu x hx, _⟩,
+  rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩,
+  rcases H ε εpos x hx with ⟨t, ht, Ht⟩,
+  exact ⟨t, ht, Ht.mono (λ n hs x hx, hε (hs x hx))⟩
+end
+
+/-- Expressing uniform convergence on a set using `dist`. -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma tendsto_uniformly_on_iff {ι : Type*}
+  {F : ι → β → α} {f : β → α} {p : filter ι} {s : set β} :
+  tendsto_uniformly_on F f p s ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x ∈ s, dist (f x) (F n x) < ε :=
+begin
+  refine ⟨λ H ε hε, H _ (dist_mem_uniformity hε), λ H u hu, _⟩,
+  rcases mem_uniformity_dist.1 hu with ⟨ε, εpos, hε⟩,
+  exact (H ε εpos).mono (λ n hs x hx, hε (hs x hx))
+end
+
+/-- Expressing locally uniform convergence using `dist`. -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma tendsto_locally_uniformly_iff {ι : Type*} [topological_space β]
+  {F : ι → β → α} {f : β → α} {p : filter ι} :
+  tendsto_locally_uniformly F f p ↔
+  ∀ ε > 0, ∀ (x : β), ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, dist (f y) (F n y) < ε :=
+by simp [← nhds_within_univ, ← tendsto_locally_uniformly_on_univ, tendsto_locally_uniformly_on_iff]
+
+/-- Expressing uniform convergence using `dist`. -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+lemma tendsto_uniformly_iff {ι : Type*}
+  {F : ι → β → α} {f : β → α} {p : filter ι} :
+  tendsto_uniformly F f p ↔ ∀ ε > 0, ∀ᶠ n in p, ∀ x, dist (f x) (F n x) < ε :=
+by { rw [← tendsto_uniformly_on_univ, tendsto_uniformly_on_iff], simp }
+
 protected lemma cauchy_iff {f : filter α} :
   cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x y ∈ t, dist x y < ε :=
 uniformity_basis_dist.cauchy_iff
@@ -606,11 +645,20 @@ begin
   exact ennreal.of_real_lt_of_real_iff_of_nonneg dist_nonneg
 end
 
+/-- Balls defined using the distance or the edistance coincide -/
+lemma metric.emetric_ball_nnreal {x : α} {ε : nnreal} : emetric.ball x ε = ball x ε :=
+by { convert metric.emetric_ball, simp }
+
 /-- Closed balls defined using the distance or the edistance coincide -/
 lemma metric.emetric_closed_ball {x : α} {ε : ℝ} (h : 0 ≤ ε) :
   emetric.closed_ball x (ennreal.of_real ε) = closed_ball x ε :=
 by ext y; simp [edist_dist]; rw ennreal.of_real_le_of_real_iff h
 
+/-- Closed balls defined using the distance or the edistance coincide -/
+lemma metric.emetric_closed_ball_nnreal {x : α} {ε : nnreal} :
+  emetric.closed_ball x ε = closed_ball x ε :=
+by { convert metric.emetric_closed_ball ε.2, simp }
+
 def metric_space.replace_uniformity {α} [U : uniform_space α] (m : metric_space α)
   (H : @uniformity _ U = @uniformity _ (metric_space.to_uniform_space α)) :
   metric_space α :=