feat(analysis): sequential completeness

analysis/metric_space.lean

@@ -329,12 +329,80 @@ theorem continuous_of_metric [metric_space β] {f : α → β} :
     ∀b (ε > 0), ∃ δ > 0, ∀a, dist a b < δ → dist (f a) (f b) < ε :=
 continuous_iff_tendsto.trans $ forall_congr $ λ b, tendsto_nhds_of_metric
 
-theorem exists_delta_of_continuous [metric_space β] {f : α → β} {ε:ℝ}
+theorem exists_delta_of_continuous [metric_space β] {f : α → β} {ε : ℝ}
   (hf : continuous f) (hε : ε > 0) (b : α) :
   ∃ δ > 0, ∀a, dist a b ≤ δ → dist (f a) (f b) < ε :=
 let ⟨δ, δ_pos, hδ⟩ := continuous_of_metric.1 hf b ε hε in
 ⟨δ / 2, half_pos δ_pos, assume a ha, hδ a $ lt_of_le_of_lt ha $ div_two_lt_of_pos δ_pos⟩
 
+theorem tendsto_nhds_topo_metric {f : filter β} {u : β → α} {a : α} :
+  tendsto u f (nhds a) ↔ ∀ ε > 0, ∃ n ∈ f.sets, ∀x ∈ n,  dist (u x) a < ε :=
+⟨λ H ε ε0, ⟨u⁻¹' (ball a ε), H (ball_mem_nhds _ ε0), by simp⟩,
+ λ H s hs,
+  let ⟨ε, ε0, hε⟩ := mem_nhds_iff_metric.1 hs, ⟨δ, δ0, hδ⟩ := H _ ε0 in
+  f.sets_of_superset δ0 (λx xδ, hε (hδ x xδ))⟩
+
+theorem continuous_topo_metric [topological_space β] {f : β → α} :
+  continuous f ↔ ∀a (ε > 0), ∃ n ∈ (nhds a).sets, ∀b ∈ n, dist (f b) (f a) < ε :=
+continuous_iff_tendsto.trans $ forall_congr $ λ b, tendsto_nhds_topo_metric
+
+theorem tendsto_at_top_metric [inhabited β] [semilattice_sup β] (u : β → α) {a : α} :
+  tendsto u at_top (nhds a) ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) a < ε :=
+begin
+  rw tendsto_nhds_topo_metric,
+  apply forall_congr,
+  intro ε,
+  apply forall_congr,
+  intro hε,
+  simp,
+  exact ⟨λ ⟨s, ⟨N, hN⟩, hs⟩, ⟨N, λn hn, hs _ (hN _ hn)⟩, λ ⟨N, hN⟩, ⟨{n | n ≥ N}, ⟨⟨N, by simp⟩, hN⟩⟩⟩,
+end
+
+section cauchy_seq
+variables [inhabited β] [semilattice_sup β]
+
+/--In a metric space, Cauchy sequences are characterized by the fact that, eventually,
+the distance between its elements is arbitrarily small-/
+theorem cauchy_seq_metric {u : β → α} :
+  cauchy_seq u ↔ ∀ε>0, ∃N, ∀m n≥N, dist (u n) (u m) < ε :=
+begin
+  unfold cauchy_seq,
+  rw cauchy_of_metric,
+  simp,
+  split,
+  { intros H ε εpos,
+    rcases H ε εpos with ⟨t, ⟨N, hN⟩, ht⟩,
+    exact ⟨N, λm n hm hn, ht _ _ (hN _ hn) (hN _ hm)⟩ },
+  { intros H ε εpos,
+    rcases H (ε/2) (half_pos εpos) with ⟨N, hN⟩,
+    existsi ball (u N) (ε/2),
+    split,
+    { exact ⟨N, λx hx, hN _ _ (le_refl N) hx⟩ },
+    { exact λx y hx hy, calc
+        dist x y ≤ dist x (u N) + dist y (u N) : dist_triangle_right _ _ _
+        ... < ε/2 + ε/2 : add_lt_add hx hy
+        ... = ε : add_halves _ } }
+end
+
+/--A variation around the metric characterization of Cauchy sequences-/
+theorem cauchy_seq_metric' {u : β → α} :
+  cauchy_seq u ↔ ∀ε>0, ∃N, ∀n≥N, dist (u n) (u N) < ε :=
+begin
+  rw cauchy_seq_metric,
+  split,
+  { intros H ε εpos,
+    rcases H ε εpos with ⟨N, hN⟩,
+    exact ⟨N, λn hn, hN _ _ (le_refl N) hn⟩ },
+  { intros H ε εpos,
+    rcases H (ε/2) (half_pos εpos) with ⟨N, hN⟩,
+    exact ⟨N, λ m n hm hn, calc
+       dist (u n) (u m) ≤ dist (u n) (u N) + dist (u m) (u N) : dist_triangle_right _ _ _
+                    ... < ε/2 + ε/2 : add_lt_add (hN _ hn) (hN _ hm)
+                    ... = ε : add_halves _⟩ }
+end
+
+end cauchy_seq
+
 theorem eq_of_forall_dist_le {x y : α} (h : ∀ε, ε > 0 → dist x y ≤ ε) : x = y :=
 eq_of_dist_eq_zero (eq_of_le_of_forall_le_of_dense dist_nonneg h)
 

analysis/topology/uniform_space.lean

@@ -844,11 +844,21 @@ begin
   exact assume f hf hfs, hc (ht _ hf hfs) hfs
 end
 
+/--Cauchy sequences. Usually defined on ℕ, but often it is also useful to say that a function
+defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it in a type class that
+is general enough to cover both ℕ and ℝ, which are the main motivating examples.-/
+def cauchy_seq [inhabited β] [semilattice_sup β] (u : β → α) := cauchy (at_top.map u)
+
 /-- A complete space is defined here using uniformities. A uniform space
   is complete if every Cauchy filter converges. -/
 class complete_space (α : Type u) [uniform_space α] : Prop :=
 (complete : ∀{f:filter α}, cauchy f → ∃x, f ≤ nhds x)
 
+/--A Cauchy sequence in a complete space converges-/
+theorem cauchy_seq_tendsto_of_complete [inhabited β] [semilattice_sup β] [complete_space α]
+  {u : β → α} (H : cauchy_seq u) : ∃x, tendsto u at_top (nhds x)
+:= complete_space.complete H
+
 theorem le_nhds_lim_of_cauchy {α} [uniform_space α] [complete_space α]
   [inhabited α] {f : filter α} (hf : cauchy f) : f ≤ nhds (lim f) :=
 lim_spec (complete_space.complete hf)