feat(topology/uniform_space/equicontinuity): definition and basic pro…

…perties of [uniform] equicontinuity (#16467)

src/topology/continuous_function/bounded.lean

@@ -8,6 +8,7 @@ import analysis.normed_space.operator_norm
 import analysis.normed_space.star.basic
 import data.real.sqrt
 import topology.continuous_function.algebra
+import topology.metric_space.equicontinuity
 
 /-!
 # Bounded continuous functions
@@ -18,7 +19,7 @@ the uniform distance.
 -/
 
 noncomputable theory
-open_locale topological_space classical nnreal
+open_locale topological_space classical nnreal uniformity uniform_convergence
 
 open set filter metric function
 
@@ -226,6 +227,20 @@ iff.intro
     λ n hn, lt_of_le_of_lt ((dist_le (half_pos ε_pos).le).mpr $
     λ x, dist_comm (f x) (F n x) ▸ le_of_lt (hn x)) (half_lt_self ε_pos)))
 
+/-- The topology on `α →ᵇ β` is exactly the topology induced by the natural map to `α →ᵤ β`. -/
+lemma inducing_coe_fn : inducing (uniform_fun.of_fun ∘ coe_fn : (α →ᵇ β) → (α →ᵤ β)) :=
+begin
+  rw inducing_iff_nhds,
+  refine λ f, eq_of_forall_le_iff (λ l, _),
+  rw [← tendsto_iff_comap, ← tendsto_id', tendsto_iff_tendsto_uniformly,
+      uniform_fun.tendsto_iff_tendsto_uniformly],
+  refl
+end
+
+-- TODO: upgrade to a `uniform_embedding`
+lemma embedding_coe_fn : embedding (uniform_fun.of_fun ∘ coe_fn : (α →ᵇ β) → (α →ᵤ β)) :=
+⟨inducing_coe_fn, λ f g h, ext $ λ x, congr_fun h x⟩
+
 variables (α) {β}
 
 /-- Constant as a continuous bounded function. -/
@@ -417,10 +432,10 @@ and several useful variations around it. -/
 theorem arzela_ascoli₁ [compact_space β]
   (A : set (α →ᵇ β))
   (closed : is_closed A)
-  (H : ∀ (x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
-    f ∈ A → dist (f y) (f z) < ε) :
+  (H : equicontinuous (coe_fn : A → α → β)) :
   is_compact A :=
 begin
+  simp_rw [equicontinuous, metric.equicontinuous_at_iff_pair] at H,
   refine is_compact_of_totally_bounded_is_closed _ closed,
   refine totally_bounded_of_finite_discretization (λ ε ε0, _),
   rcases exists_between ε0 with ⟨ε₁, ε₁0, εε₁⟩,
@@ -437,7 +452,7 @@ begin
     f ∈ A → dist (f y) (f z) < ε₂ := λ x,
       let ⟨U, nhdsU, hU⟩ := H x _ ε₂0,
           ⟨V, VU, openV, xV⟩ := _root_.mem_nhds_iff.1 nhdsU in
-      ⟨V, xV, openV, λy hy z hz f hf, hU y (VU hy) z (VU hz) f hf⟩,
+      ⟨V, xV, openV, λy hy z hz f hf, hU y (VU hy) z (VU hz) ⟨f, hf⟩⟩,
   choose U hU using this,
   /- For all x, the set hU x is an open set containing x on which the elements of A
   fluctuate by at most ε₂.
@@ -481,8 +496,7 @@ theorem arzela_ascoli₂
   (A : set (α →ᵇ β))
   (closed : is_closed A)
   (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
-  (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
-    f ∈ A → dist (f y) (f z) < ε) :
+  (H : equicontinuous (coe_fn : A → α → β)) :
   is_compact A :=
 /- This version is deduced from the previous one by restricting to the compact type in the target,
 using compactness there and then lifting everything to the original space. -/
@@ -492,10 +506,9 @@ begin
   refine is_compact_of_is_closed_subset
     ((_ : is_compact (F ⁻¹' A)).image (continuous_comp M)) closed (λ f hf, _),
   { haveI : compact_space s := is_compact_iff_compact_space.1 hs,
-    refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed)
-      (λ x ε ε0, bex.imp_right (λ U U_nhds hU y hy z hz f hf, _) (H x ε ε0)),
-    calc dist (f y) (f z) = dist (F f y) (F f z) : rfl
-                        ... < ε : hU y hy z hz (F f) hf },
+    refine arzela_ascoli₁ _ (continuous_iff_is_closed.1 (continuous_comp M) _ closed) _,
+    rw uniform_embedding_subtype_coe.to_uniform_inducing.equicontinuous_iff,
+    exact H.comp (A.restrict_preimage F) },
   { let g := cod_restrict s f (λx, in_s f x hf),
     rw [show f = F g, by ext; refl] at hf ⊢,
     exact ⟨g, hf, rfl⟩ }
@@ -507,51 +520,15 @@ theorem arzela_ascoli [t2_space β]
   (s : set β) (hs : is_compact s)
   (A : set (α →ᵇ β))
   (in_s : ∀(f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s)
-  (H : ∀(x:α) (ε > 0), ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
-    f ∈ A → dist (f y) (f z) < ε) :
+  (H : equicontinuous (coe_fn : A → α → β)) :
   is_compact (closure A) :=
 /- This version is deduced from the previous one by checking that the closure of A, in
 addition to being closed, still satisfies the properties of compact range and equicontinuity -/
 arzela_ascoli₂ s hs (closure A) is_closed_closure
   (λ f x hf, (mem_of_closed' hs.is_closed).2 $ λ ε ε0,
     let ⟨g, gA, dist_fg⟩ := metric.mem_closure_iff.1 hf ε ε0 in
     ⟨g x, in_s g x gA, lt_of_le_of_lt (dist_coe_le_dist _) dist_fg⟩)
-  (λ x ε ε0, show ∃ U ∈ 𝓝 x,
-      ∀ y z ∈ U, ∀ (f : α →ᵇ β), f ∈ closure A → dist (f y) (f z) < ε,
-    begin
-      refine bex.imp_right (λ U U_set hU y hy z hz f hf, _) (H x (ε/2) (half_pos ε0)),
-      rcases metric.mem_closure_iff.1 hf (ε/2/2) (half_pos (half_pos ε0)) with ⟨g, gA, dist_fg⟩,
-      replace dist_fg := λ x, lt_of_le_of_lt (dist_coe_le_dist x) dist_fg,
-      calc dist (f y) (f z) ≤ dist (f y) (g y) + dist (f z) (g z) + dist (g y) (g z) :
-        dist_triangle4_right _ _ _ _
-          ... < ε/2/2 + ε/2/2 + ε/2 :
-            add_lt_add (add_lt_add (dist_fg y) (dist_fg z)) (hU y hy z hz g gA)
-          ... = ε : by rw [add_halves, add_halves]
-    end)
-
-/- To apply the previous theorems, one needs to check the equicontinuity. An important
-instance is when the source space is a metric space, and there is a fixed modulus of continuity
-for all the functions in the set A -/
-
-lemma equicontinuous_of_continuity_modulus {α : Type u} [pseudo_metric_space α]
-  (b : ℝ → ℝ) (b_lim : tendsto b (𝓝 0) (𝓝 0))
-  (A : set (α →ᵇ β))
-  (H : ∀(x y:α) (f : α →ᵇ β), f ∈ A → dist (f x) (f y) ≤ b (dist x y))
-  (x:α) (ε : ℝ) (ε0 : 0 < ε) : ∃U ∈ 𝓝 x, ∀ (y z ∈ U) (f : α →ᵇ β),
-    f ∈ A → dist (f y) (f z) < ε :=
-begin
-  rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩,
-  refine ⟨ball x (δ/2), ball_mem_nhds x (half_pos δ0), λ y hy z hz f hf, _⟩,
-  have : dist y z < δ := calc
-    dist y z ≤ dist y x + dist z x : dist_triangle_right _ _ _
-    ... < δ/2 + δ/2 : add_lt_add hy hz
-    ... = δ : add_halves _,
-  calc
-    dist (f y) (f z) ≤ b (dist y z) : H y z f hf
-    ... ≤ |b (dist y z)| : le_abs_self _
-    ... = dist (b (dist y z)) 0 : by simp [real.dist_eq]
-    ... < ε : hδ (by simpa [real.dist_eq] using this),
-end
+  (H.closure' continuous_coe)
 
 end arzela_ascoli
 

src/topology/metric_space/equicontinuity.lean

@@ -0,0 +1,127 @@
+/-
+Copyright (c) 2022 Anatole Dedecker. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Anatole Dedecker
+-/
+
+import topology.metric_space.basic
+import topology.uniform_space.equicontinuity
+/-!
+# Equicontinuity in metric spaces
+
+This files contains various facts about (uniform) equicontinuity in metric spaces. Most
+importantly, we prove the usual characterization of equicontinuity of `F` at `x₀` in the case of
+(pseudo) metric spaces: `∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε`,
+and we prove that functions sharing a common (local or global) continuity modulus are
+(locally or uniformly) equicontinuous.
+
+## Main statements
+
+* `equicontinuous_at_iff`: characterization of equicontinuity for families of functions between
+  (pseudo) metric spaces.
+* `equicontinuous_at_of_continuity_modulus`: convenient way to prove equicontinuity at a point of
+  a family of functions to a (pseudo) metric space by showing that they share a common *local*
+  continuity modulus.
+* `uniform_equicontinuous_of_continuity_modulus`: convenient way to prove uniform equicontinuity
+  of a family of functions to a (pseudo) metric space by showing that they share a common *global*
+  continuity modulus.
+
+## Tags
+
+equicontinuity, continuity modulus
+-/
+
+open filter
+open_locale topological_space uniformity
+
+variables {α β ι : Type*} [pseudo_metric_space α]
+
+namespace metric
+
+/-- Characterization of equicontinuity for families of functions taking values in a (pseudo) metric
+space. -/
+lemma equicontinuous_at_iff_right {ι : Type*} [topological_space β] {F : ι → β → α} {x₀ : β} :
+  equicontinuous_at F x₀ ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 x₀, ∀ i, dist (F i x₀) (F i x) < ε :=
+uniformity_basis_dist.equicontinuous_at_iff_right
+
+/-- Characterization of equicontinuity for families of functions between (pseudo) metric spaces. -/
+lemma equicontinuous_at_iff {ι : Type*} [pseudo_metric_space β] {F : ι → β → α} {x₀ : β} :
+  equicontinuous_at F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε :=
+nhds_basis_ball.equicontinuous_at_iff uniformity_basis_dist
+
+/-- Reformulation of `equicontinuous_at_iff_pair` for families of functions taking values in a
+(pseudo) metric space. -/
+protected lemma equicontinuous_at_iff_pair {ι : Type*} [topological_space β] {F : ι → β → α}
+  {x₀ : β} :
+  equicontinuous_at F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ (x x' ∈ U), ∀ i, dist (F i x) (F i x') < ε :=
+begin
+  rw equicontinuous_at_iff_pair,
+  split; intros H,
+  { intros ε hε,
+    refine exists_imp_exists (λ V, exists_imp_exists $ λ hV h, _) (H _ (dist_mem_uniformity hε)),
+    exact λ x hx x' hx', h _ hx _ hx' },
+  { intros U hU,
+    rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩,
+    refine exists_imp_exists (λ V, exists_imp_exists $ λ hV h, _) (H _ hε),
+    exact λ x hx x' hx' i, hεU (h _ hx _ hx' i) }
+end
+
+/-- Characterization of uniform equicontinuity for families of functions taking values in a
+(pseudo) metric space. -/
+lemma uniform_equicontinuous_iff_right {ι : Type*} [uniform_space β] {F : ι → β → α} :
+  uniform_equicontinuous F ↔
+  ∀ ε > 0, ∀ᶠ (xy : β × β) in 𝓤 β, ∀ i, dist (F i xy.1) (F i xy.2) < ε :=
+uniformity_basis_dist.uniform_equicontinuous_iff_right
+
+/-- Characterization of uniform equicontinuity for families of functions between
+(pseudo) metric spaces. -/
+lemma uniform_equicontinuous_iff {ι : Type*} [pseudo_metric_space β] {F : ι → β → α} :
+  uniform_equicontinuous F ↔
+  ∀ ε > 0, ∃ δ > 0, ∀ x y, dist x y < δ → ∀ i, dist (F i x) (F i y) < ε :=
+uniformity_basis_dist.uniform_equicontinuous_iff uniformity_basis_dist
+
+/-- For a family of functions to a (pseudo) metric spaces, a convenient way to prove
+equicontinuity at a point is to show that all of the functions share a common *local* continuity
+modulus. -/
+lemma equicontinuous_at_of_continuity_modulus {ι : Type*} [topological_space β] {x₀ : β}
+  (b : β → ℝ)
+  (b_lim : tendsto b (𝓝 x₀) (𝓝 0))
+  (F : ι → β → α)
+  (H : ∀ᶠ x in 𝓝 x₀, ∀ i, dist (F i x₀) (F i x) ≤ b x) :
+  equicontinuous_at F x₀ :=
+begin
+  rw metric.equicontinuous_at_iff_right,
+  intros ε ε0,
+  filter_upwards [b_lim (Iio_mem_nhds ε0), H] using λ x hx₁ hx₂ i, (hx₂ i).trans_lt hx₁
+end
+
+/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
+uniform equicontinuity is to show that all of the functions share a common *global* continuity
+modulus. -/
+lemma uniform_equicontinuous_of_continuity_modulus {ι : Type*} [pseudo_metric_space β] (b : ℝ → ℝ)
+  (b_lim : tendsto b (𝓝 0) (𝓝 0))
+  (F : ι → β → α)
+  (H : ∀ (x y : β) i, dist (F i x) (F i y) ≤ b (dist x y)) :
+  uniform_equicontinuous F :=
+begin
+  rw metric.uniform_equicontinuous_iff,
+  intros ε ε0,
+  rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩,
+  refine ⟨δ, δ0, λ x y hxy i, _⟩,
+  calc
+    dist (F i x) (F i y) ≤ b (dist x y) : H x y i
+    ... ≤ |b (dist x y)| : le_abs_self _
+    ... = dist (b (dist x y)) 0 : by simp [real.dist_eq]
+    ... < ε : hδ (by simpa only [real.dist_eq, tsub_zero, abs_dist] using hxy)
+end
+
+/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
+equicontinuity is to show that all of the functions share a common *global* continuity modulus. -/
+lemma equicontinuous_of_continuity_modulus {ι : Type*} [pseudo_metric_space β] (b : ℝ → ℝ)
+  (b_lim : tendsto b (𝓝 0) (𝓝 0))
+  (F : ι → β → α)
+  (H : ∀ (x y : β) i, dist (F i x) (F i y) ≤ b (dist x y)) :
+  equicontinuous F :=
+(uniform_equicontinuous_of_continuity_modulus b b_lim F H).equicontinuous
+
+end metric

src/topology/metric_space/gromov_hausdorff_realized.lean

@@ -269,7 +269,7 @@ begin
     { have : tendsto (λ (t : ℝ), 2 * (max_var X Y : ℝ) * t) (𝓝 0) (𝓝 (2 * max_var X Y * 0)) :=
         tendsto_const_nhds.mul tendsto_id,
       simpa using this },
-    { assume x y f hf,
+    { rintros x y ⟨f, hf⟩,
       exact (candidates_lipschitz hf).dist_le_mul _ _ } }
 end
 

src/topology/uniform_space/compact.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Yury Kudryashov
 -/
 import topology.uniform_space.uniform_convergence
+import topology.uniform_space.equicontinuity
 import topology.separation
 
 /-!
@@ -178,7 +179,7 @@ def uniform_space_of_compact_t2 [topological_space γ] [compact_space γ] [t2_sp
 ### Heine-Cantor theorem
 -/
 
-/-- Heine-Cantor: a continuous function on a compact separated uniform space is uniformly
+/-- Heine-Cantor: a continuous function on a compact uniform space is uniformly
 continuous. -/
 lemma compact_space.uniform_continuous_of_continuous [compact_space α]
   {f : α → β} (h : continuous f) : uniform_continuous f :=
@@ -220,3 +221,18 @@ locally compact and `β` is compact. -/
 lemma continuous.tendsto_uniformly [locally_compact_space α] [compact_space β] [uniform_space γ]
   (f : α → β → γ) (h : continuous ↿f) (x : α) : tendsto_uniformly f (f x) (𝓝 x) :=
 h.continuous_on.tendsto_uniformly univ_mem
+
+section uniform_convergence
+
+/-- An equicontinuous family of functions defined on a compact uniform space is automatically
+uniformly equicontinuous. -/
+lemma compact_space.uniform_equicontinuous_of_equicontinuous {ι : Type*} {F : ι → β → α}
+  [compact_space β] (h : equicontinuous F) :
+  uniform_equicontinuous F :=
+begin
+  rw equicontinuous_iff_continuous at h,
+  rw uniform_equicontinuous_iff_uniform_continuous,
+  exact compact_space.uniform_continuous_of_continuous h
+end
+
+end uniform_convergence