feat(analysis/{specific_limits,infinite_sum}): Cauchy of geometric bo…

…und (#753)

src/analysis/specific_limits.lean

@@ -112,6 +112,26 @@ begin
   { assume n, exact le_refl _ }
 end
 
+lemma cauchy_seq_of_le_geometric [metric_space α] (r C : ℝ) (hr : r < 1) {f : ℕ → α}
+  (hu : ∀n, dist (f n) (f (n+1)) ≤ C * r^n) : cauchy_seq f :=
+begin
+  refine cauchy_seq_of_has_sum_dist (has_sum_of_norm_bounded (λn, C * r^n) _ _),
+  { by_cases h : C = 0,
+    { simp [h, has_sum_zero] },
+    { have Cpos : C > 0,
+      { have := le_trans dist_nonneg (hu 0),
+        simp only [mul_one, pow_zero] at this,
+        exact lt_of_le_of_ne this (ne.symm h) },
+      have rnonneg: r ≥ 0,
+      { have := le_trans dist_nonneg (hu 1),
+        simp only [pow_one] at this,
+        exact nonneg_of_mul_nonneg_left this Cpos },
+      refine has_sum_mul_left C _,
+      exact has_sum_spec (@is_sum_geometric r rnonneg hr) }},
+  show ∀n, abs (dist (f n) (f (n+1))) ≤ C * r^n,
+  { assume n, rw abs_of_nonneg (dist_nonneg), exact hu n }
+end
+
 namespace nnreal
 
 theorem exists_pos_sum_of_encodable {ε : nnreal} (hε : 0 < ε) (ι) [encodable ι] :

src/topology/algebra/infinite_sum.lean

@@ -18,6 +18,7 @@ Reference:
 -/
 import logic.function algebra.big_operators data.set data.finset
        topology.metric_space.basic topology.algebra.topological_structures
+       topology.instances.real
 
 noncomputable theory
 open lattice finset filter function classical
@@ -509,3 +510,33 @@ end,
 has_sum_of_has_sum_of_sub _ _ hf $ assume b, by by_cases b ∈ set.range i; simp [h]
 
 end uniform_group
+
+section cauchy_seq
+open finset.Ico filter
+
+lemma cauchy_seq_of_has_sum_dist [metric_space α] {f : ℕ → α}
+  (h : has_sum (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
+begin
+  let d := λn, dist (f n) (f (n+1)),
+  refine metric.cauchy_seq_iff'.2 (λε εpos, _),
+  rcases (has_sum_iff_vanishing _).1 h {x : ℝ | x < ε} (gt_mem_nhds εpos) with ⟨s, hs⟩,
+  have : ∃N:ℕ, ∀x ∈ s, x < N,
+  { by_cases h : s = ∅,
+    { use 0, simp [h]},
+    { use s.max' h + 1,
+      exact λx hx, lt_of_le_of_lt (s.le_max' h x hx) (nat.lt_succ_self _) }},
+  rcases this with ⟨N, hN⟩,
+  refine ⟨N, λn hn, _⟩,
+  have : ∀n, n ≥ N → dist (f N) (f n) ≤ (Ico N n).sum d,
+  { apply nat.le_induction,
+    { simp },
+    { assume n hn hrec,
+      calc dist (f N) (f (n+1)) ≤ dist (f N) (f n) + d n : dist_triangle _ _ _
+        ... ≤ (Ico N n).sum d + d n : add_le_add hrec (le_refl _)
+        ... = (Ico N (n+1)).sum d : by rw [succ_top hn, sum_insert, add_comm]; simp }},
+  calc dist (f n) (f N) ≤ (Ico N n).sum d : by rw dist_comm; apply this n hn
+    ... < ε : hs _ (finset.disjoint_iff_ne.2
+                     (λa ha b hb, ne_of_gt (lt_of_lt_of_le (hN _ hb) (mem.1 ha).1)))
+end
+
+end cauchy_seq