feat(topology/uniform_space/uniform_convergence): Uniform Cauchy sequ…

…ences (#14003)

A sequence of functions `f_n` is pointwise Cauchy if `∀x ∀ε ∃N ∀(m, n) > N` we have `|f_m x - f_n x| < ε`. A sequence of functions is _uniformly_ Cauchy if `∀ε ∃N ∀(m, n) > N ∀x` we have `|f_m x - f_n x| < ε`.

As a sequence of functions is pointwise Cauchy if (and when the underlying space is complete, only if) the sequence converges, a sequence of functions is uniformly Cauchy if (and when the underlying space is complete, only if) the sequence uniformly converges. (Note that the parenthetical is not directly covered by this commit, but is an easy consequence of two of its lemmas.)

This notion is commonly used to bootstrap convergence into uniform convergence.

src/topology/metric_space/basic.lean

@@ -1256,6 +1256,34 @@ theorem metric.cauchy_seq_iff' {u : β → α} :
   cauchy_seq u ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) (u N) < ε :=
 uniformity_basis_dist.cauchy_seq_iff'
 
+/-- In a pseudometric space, unifom Cauchy sequences are characterized by the fact that, eventually,
+the distance between all its elements is uniformly, arbitrarily small -/
+@[nolint ge_or_gt] -- see Note [nolint_ge]
+theorem metric.uniform_cauchy_seq_on_iff {γ : Type*}
+  {F : β → γ → α} {s : set γ} :
+  uniform_cauchy_seq_on F at_top s ↔
+    ∀ ε : ℝ, ε > 0 → ∃ (N : β), ∀ m : β, m ≥ N → ∀ n : β, n ≥ N → ∀ x : γ, x ∈ s →
+    dist (F m x) (F n x) < ε :=
+begin
+  split,
+  { intros h ε hε,
+    let u := { a : α × α | dist a.fst a.snd < ε },
+    have hu : u ∈ 𝓤 α := metric.mem_uniformity_dist.mpr ⟨ε, hε, (λ a b, by simp)⟩,
+    rw ←@filter.eventually_at_top_prod_self' _ _ _
+      (λ m, ∀ x : γ, x ∈ s → dist (F m.fst x) (F m.snd x) < ε),
+    specialize h u hu,
+    rw prod_at_top_at_top_eq at h,
+    exact h.mono (λ n h x hx, set.mem_set_of_eq.mp (h x hx)), },
+  { intros h u hu,
+    rcases (metric.mem_uniformity_dist.mp hu) with ⟨ε, hε, hab⟩,
+    rcases h ε hε with ⟨N, hN⟩,
+    rw [prod_at_top_at_top_eq, eventually_at_top],
+    use (N, N),
+    intros b hb x hx,
+    rcases hb with ⟨hbl, hbr⟩,
+    exact hab (hN b.fst hbl.ge b.snd hbr.ge x hx), },
+end
+
 /-- If the distance between `s n` and `s m`, `n ≤ m` is bounded above by `b n`
 and `b` converges to zero, then `s` is a Cauchy sequence.  -/
 lemma cauchy_seq_of_le_tendsto_0' {s : β → α} (b : β → ℝ)

src/topology/uniform_space/uniform_convergence.lean

@@ -36,6 +36,9 @@ We also define notions where the convergence is locally uniform, called
 `tendsto_locally_uniformly_on F f p s` and `tendsto_locally_uniformly F f p`. The previous theorems
 all have corresponding versions under locally uniform convergence.
 
+Finally, we introduce the notion of a uniform Cauchy sequence, which is to uniform
+convergence what a Cauchy sequence is to the usual notion of convergence.
+
 ## Implementation notes
 
 Most results hold under weaker assumptions of locally uniform approximation. In a first section,
@@ -200,6 +203,54 @@ lemma uniform_continuous₂.tendsto_uniformly [uniform_space α] [uniform_space
 uniform_continuous_on.tendsto_uniformly univ_mem $
   by rwa [univ_prod_univ, uniform_continuous_on_univ]
 
+/-- A sequence is uniformly Cauchy if eventually all of its pairwise differences are
+uniformly bounded -/
+def uniform_cauchy_seq_on
+  (F : ι → α → β) (p : filter ι) (s : set α) : Prop :=
+  ∀ u : set (β × β), u ∈ 𝓤 β → ∀ᶠ (m : ι × ι) in (p ×ᶠ p),
+    ∀ (x : α), x ∈ s → (F m.fst x, F m.snd x) ∈ u
+
+/-- A sequence that converges uniformly is also uniformly Cauchy -/
+lemma tendsto_uniformly_on.uniform_cauchy_seq_on (hF : tendsto_uniformly_on F f p s) :
+  uniform_cauchy_seq_on F p s :=
+begin
+  intros u hu,
+  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩,
+  apply ((hF t ht).prod_mk (hF t ht)).mono,
+  intros n h x hx,
+  cases h with hl hr,
+  specialize hl x hx,
+  specialize hr x hx,
+  exact set.mem_of_mem_of_subset (prod_mk_mem_comp_rel (htsymm hl) hr) htmem,
+end
+
+/-- A uniformly Cauchy sequence converges uniformly to its limit -/
+lemma uniform_cauchy_seq_on.tendsto_uniformly_on_of_tendsto [ne_bot p]
+  (hF : uniform_cauchy_seq_on F p s) (hF' : ∀ x : α, x ∈ s → tendsto (λ n, F n x) p (nhds (f x))) :
+  tendsto_uniformly_on F f p s :=
+begin
+  -- Proof idea: |f_n(x) - f(x)| ≤ |f_n(x) - f_m(x)| + |f_m(x) - f(x)|. We choose `n`
+  -- so that |f_n(x) - f_m(x)| is uniformly small across `s` whenever `m ≥ n`. Then for
+  -- a fixed `x`, we choose `m` sufficiently large such that |f_m(x) - f(x)| is small.
+  intros u hu,
+  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩,
+
+  -- Choose n
+  apply (hF t ht).curry.mono,
+
+  -- Work with a specific x
+  intros n hn x hx,
+  refine set.mem_of_mem_of_subset (mem_comp_rel.mpr _) htmem,
+
+  -- Choose m
+  specialize hF' x hx,
+  rw uniform.tendsto_nhds_right at hF',
+  rcases (hn.and (hF'.eventually (eventually_mem_set.mpr ht))).exists with ⟨m, hm, hm'⟩,
+
+  -- Finish the proof
+  exact ⟨F m x, ⟨hm', htsymm (hm x hx)⟩⟩,
+end
+
 section seq_tendsto
 
 lemma tendsto_uniformly_on_of_seq_tendsto_uniformly_on {l : filter ι} [l.is_countably_generated]