feat(topology/algebra/infinite_sum): prove `cauchy_seq_of_edist_le_of…

…_summable` (#1739)

* feat(topology/algebra/infinite_sum): prove `cauchy_seq_of_edist_le_of_summable`

Other changes:

* Add estimates on the distance to the limit (`dist` version only)
* Simplify some proofs
* Add some supporting lemmas
* Fix a typo in a lemma name in `ennreal`

* Add `move_cast` attrs

* More `*_cast` tags, use `norm_cast`

src/data/real/ennreal.lean

@@ -109,29 +109,33 @@ by simp [ennreal.to_real, to_nnreal_eq_zero_iff]
 @[simp] lemma one_ne_top : 1 ≠ ∞ := coe_ne_top
 @[simp] lemma top_ne_one : ∞ ≠ 1 := top_ne_coe
 
-@[simp] lemma coe_eq_coe : (↑r : ennreal) = ↑q ↔ r = q := with_top.coe_eq_coe
-@[simp] lemma coe_le_coe : (↑r : ennreal) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe
-@[simp] lemma coe_lt_coe : (↑r : ennreal) < ↑q ↔ r < q := with_top.coe_lt_coe
+@[simp, elim_cast] lemma coe_eq_coe : (↑r : ennreal) = ↑q ↔ r = q := with_top.coe_eq_coe
+@[simp, elim_cast] lemma coe_le_coe : (↑r : ennreal) ≤ ↑q ↔ r ≤ q := with_top.coe_le_coe
+@[simp, elim_cast] lemma coe_lt_coe : (↑r : ennreal) < ↑q ↔ r < q := with_top.coe_lt_coe
+lemma coe_mono : monotone (coe : nnreal → ennreal) := λ _ _, coe_le_coe.2
 
-@[simp] lemma coe_eq_zero : (↑r : ennreal) = 0 ↔ r = 0 := coe_eq_coe
-@[simp] lemma zero_eq_coe : 0 = (↑r : ennreal) ↔ 0 = r := coe_eq_coe
-@[simp] lemma coe_eq_one : (↑r : ennreal) = 1 ↔ r = 1 := coe_eq_coe
-@[simp] lemma one_eq_coe : 1 = (↑r : ennreal) ↔ 1 = r := coe_eq_coe
-@[simp] lemma coe_nonneg : 0 ≤ (↑r : ennreal) ↔ 0 ≤ r := coe_le_coe
-@[simp] lemma coe_pos : 0 < (↑r : ennreal) ↔ 0 < r := coe_lt_coe
+@[simp, elim_cast] lemma coe_eq_zero : (↑r : ennreal) = 0 ↔ r = 0 := coe_eq_coe
+@[simp, elim_cast] lemma zero_eq_coe : 0 = (↑r : ennreal) ↔ 0 = r := coe_eq_coe
+@[simp, elim_cast] lemma coe_eq_one : (↑r : ennreal) = 1 ↔ r = 1 := coe_eq_coe
+@[simp, elim_cast] lemma one_eq_coe : 1 = (↑r : ennreal) ↔ 1 = r := coe_eq_coe
+@[simp, elim_cast] lemma coe_nonneg : 0 ≤ (↑r : ennreal) ↔ 0 ≤ r := coe_le_coe
+@[simp, elim_cast] lemma coe_pos : 0 < (↑r : ennreal) ↔ 0 < r := coe_lt_coe
 
-@[simp] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add
-@[simp] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul
+@[simp, move_cast] lemma coe_add : ↑(r + p) = (r + p : ennreal) := with_top.coe_add
+@[simp, move_cast] lemma coe_mul : ↑(r * p) = (r * p : ennreal) := with_top.coe_mul
 
-@[simp] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add
-@[simp] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1]
+@[simp, move_cast] lemma coe_bit0 : (↑(bit0 r) : ennreal) = bit0 r := coe_add
+@[simp, move_cast] lemma coe_bit1 : (↑(bit1 r) : ennreal) = bit1 r := by simp [bit1]
 
 @[simp] lemma add_top : a + ∞ = ∞ := with_top.add_top
 @[simp] lemma top_add : ∞ + a = ∞ := with_top.top_add
 
 instance : is_semiring_hom (coe : nnreal → ennreal) :=
 by refine_struct {..}; simp
 
+@[simp, move_cast] lemma coe_pow (n : ℕ) : (↑(r^n) : ennreal) = r^n :=
+is_monoid_hom.map_pow coe r n
+
 lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _
 lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _
 
@@ -164,10 +168,12 @@ with_top.mul_eq_top_iff
 lemma mul_lt_top {a b : ennreal}  : a < ⊤ → b < ⊤ → a * b < ⊤ :=
 by simp [ennreal.lt_top_iff_ne_top, (≠), mul_eq_top] {contextual := tt}
 
-@[simp] lemma coe_finset_sum {s : finset α} {f : α → nnreal} : ↑(s.sum f) = (s.sum (λa, f a) : ennreal) :=
+@[simp, move_cast] lemma coe_finset_sum {s : finset α} {f : α → nnreal} :
+  ↑(s.sum f) = (s.sum (λa, f a) : ennreal) :=
 (finset.sum_hom coe).symm
 
-@[simp] lemma coe_finset_prod {s : finset α} {f : α → nnreal} : ↑(s.prod f) = (s.prod (λa, f a) : ennreal) :=
+@[simp, move_cast] lemma coe_finset_prod {s : finset α} {f : α → nnreal} :
+  ↑(s.prod f) = (s.prod (λa, f a) : ennreal) :=
 (finset.prod_hom coe).symm
 
 @[simp] lemma bot_eq_zero : (⊥ : ennreal) = 0 := rfl
@@ -179,7 +185,7 @@ section order
 @[simp] lemma one_le_coe_iff : (1:ennreal) ≤ ↑r ↔ 1 ≤ r := coe_le_coe
 @[simp] lemma coe_le_one_iff : ↑r ≤ (1:ennreal) ↔ r ≤ 1 := coe_le_coe
 @[simp] lemma coe_lt_one_iff : (↑p : ennreal) < 1 ↔ p < 1 := coe_lt_coe
-@[simp] lemma one_lt_zero_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe
+@[simp] lemma one_lt_coe_iff : 1 < (↑p : ennreal) ↔ 1 < p := coe_lt_coe
 @[simp] lemma coe_nat (n : nat) : ((n : nnreal) : ennreal) = n := with_top.coe_nat n
 @[simp] lemma nat_ne_top (n : nat) : (n : ennreal) ≠ ⊤ := with_top.nat_ne_top n
 @[simp] lemma top_ne_nat (n : nat) : (⊤ : ennreal) ≠ n := with_top.top_ne_nat n
@@ -255,6 +261,12 @@ begin
   apply lt_of_lt_of_le I J
 end
 
+@[move_cast] lemma coe_min : ((min r p:nnreal):ennreal) = min r p :=
+coe_mono.map_min
+
+@[move_cast] lemma coe_max : ((max r p:nnreal):ennreal) = max r p :=
+coe_mono.map_max
+
 end order
 
 section complete_lattice
@@ -301,7 +313,7 @@ end mul
 section sub
 instance : has_sub ennreal := ⟨λa b, Inf {d | a ≤ d + b}⟩
 
-lemma coe_sub : ↑(p - r) = (↑p:ennreal) - r :=
+@[move_cast] lemma coe_sub : ↑(p - r) = (↑p:ennreal) - r :=
 le_antisymm
   (le_Inf $ assume b (hb : ↑p ≤ b + r), coe_le_iff.2 $
     by rintros d rfl; rwa [← coe_add, coe_le_coe, ← nnreal.sub_le_iff_le_add] at hb)

src/data/real/nnreal.lean

@@ -53,11 +53,11 @@ instance : inhabited ℝ≥0 := ⟨0⟩
 @[simp] protected lemma coe_zero : ((0 : ℝ≥0) : ℝ) = 0 := rfl
 @[simp] protected lemma coe_one  : ((1 : ℝ≥0) : ℝ) = 1 := rfl
 @[simp] protected lemma coe_add (r₁ r₂ : ℝ≥0) : ((r₁ + r₂ : ℝ≥0) : ℝ) = r₁ + r₂ := rfl
-@[simp] protected lemma coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ := rfl
-@[simp] protected lemma coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = r₁ / r₂ := rfl
-@[simp] protected lemma coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = r⁻¹ := rfl
+@[simp, move_cast] protected lemma coe_mul (r₁ r₂ : ℝ≥0) : ((r₁ * r₂ : ℝ≥0) : ℝ) = r₁ * r₂ := rfl
+@[simp, move_cast] protected lemma coe_div (r₁ r₂ : ℝ≥0) : ((r₁ / r₂ : ℝ≥0) : ℝ) = r₁ / r₂ := rfl
+@[simp, move_cast] protected lemma coe_inv (r : ℝ≥0) : ((r⁻¹ : ℝ≥0) : ℝ) = r⁻¹ := rfl
 
-@[simp] protected lemma coe_sub (r₁ r₂ : ℝ≥0) (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ :=
+@[simp] protected lemma coe_sub {r₁ r₂ : ℝ≥0} (h : r₂ ≤ r₁) : ((r₁ - r₂ : ℝ≥0) : ℝ) = r₁ - r₂ :=
 max_eq_left $ le_sub.2 $ by simp [show (r₂ : ℝ) ≤ r₁, from h]
 
 -- TODO: setup semifield!
@@ -75,26 +75,30 @@ end
 
 instance : is_semiring_hom (coe : ℝ≥0 → ℝ) := by refine_struct {..}; intros; refl
 
-lemma sum_coe {α} {s : finset α} {f : α → ℝ≥0} : ↑(s.sum f) = s.sum (λa, (f a : ℝ)) :=
+@[move_cast] lemma coe_pow (r : ℝ≥0) (n : ℕ) : ((r^n : ℝ≥0) : ℝ) = r^n :=
+is_monoid_hom.map_pow coe r n
+
+@[move_cast] lemma sum_coe {α} {s : finset α} {f : α → ℝ≥0} :
+  ↑(s.sum f) = s.sum (λa, (f a : ℝ)) :=
 eq.symm $ finset.sum_hom _
 
-lemma prod_coe {α} {s : finset α} {f : α → ℝ≥0} : ↑(s.prod f) = s.prod (λa, (f a : ℝ)) :=
+@[move_cast] lemma prod_coe {α} {s : finset α} {f : α → ℝ≥0} :
+  ↑(s.prod f) = s.prod (λa, (f a : ℝ)) :=
 eq.symm $ finset.prod_hom _
 
-lemma smul_coe (r : ℝ≥0) : ∀n, ↑(add_monoid.smul n r) = add_monoid.smul n (r:ℝ)
-| 0       := rfl
-| (n + 1) := by simp [add_monoid.add_smul, smul_coe n]
+@[move_cast] lemma smul_coe (r : ℝ≥0) (n : ℕ) : ↑(add_monoid.smul n r) = add_monoid.smul n (r:ℝ) :=
+is_add_monoid_hom.map_smul coe r n
 
-@[simp] protected lemma coe_nat_cast : ∀(n : ℕ), (↑(↑n : ℝ≥0) : ℝ) = n
-| 0       := rfl
-| (n + 1) := by simp [coe_nat_cast n]
+@[simp, squash_cast] protected lemma coe_nat_cast (n : ℕ) : (↑(↑n : ℝ≥0) : ℝ) = n :=
+is_semiring_hom.map_nat_cast coe n
 
 instance : decidable_linear_order ℝ≥0 :=
 decidable_linear_order.lift (coe : ℝ≥0 → ℝ) subtype.val_injective (by apply_instance)
 
 @[elim_cast] protected lemma coe_le {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) ≤ r₂ ↔ r₁ ≤ r₂ := iff.rfl
 @[elim_cast] protected lemma coe_lt {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) < r₂ ↔ r₁ < r₂ := iff.rfl
 @[elim_cast] protected lemma coe_pos {r : ℝ≥0} : (0 : ℝ) < r ↔ 0 < r := iff.rfl
+@[elim_cast] protected lemma coe_eq {r₁ r₂ : ℝ≥0} : (r₁ : ℝ) = r₂ ↔ r₁ = r₂ := subtype.ext.symm
 
 protected lemma coe_mono : monotone (coe : ℝ≥0 → ℝ) := λ _ _, nnreal.coe_le.2
 
@@ -332,21 +336,26 @@ end mul
 
 section sub
 
+lemma sub_def {r p : ℝ≥0} : r - p = nnreal.of_real (r - p) := rfl
+
 lemma sub_eq_zero {r p : nnreal} (h : r ≤ p) : r - p = 0 :=
 nnreal.eq $ max_eq_right $ sub_le_iff_le_add.2 $ by simpa [nnreal.coe_le] using h
 
+lemma sub_pos {r p : ℝ≥0} : 0 < r - p ↔ p < r :=
+of_real_pos.trans $ sub_pos.trans $ nnreal.coe_lt
+
 protected lemma sub_lt_self {r p : nnreal} : 0 < r → 0 < p → r - p < r :=
 assume hr hp,
 begin
   cases le_total r p,
   { rwa [sub_eq_zero h] },
-  { rw [← nnreal.coe_lt, nnreal.coe_sub _ _ h], exact sub_lt_self _ hp }
+  { rw [← nnreal.coe_lt, nnreal.coe_sub h], exact sub_lt_self _ hp }
 end
 
 @[simp] lemma sub_le_iff_le_add {r p q : nnreal} : r - p ≤ q ↔ r ≤ q + p :=
 match le_total p r with
 | or.inl h :=
-  by rw [← nnreal.coe_le, ← nnreal.coe_le, nnreal.coe_sub _ _ h, nnreal.coe_add, sub_le_iff_le_add]
+  by rw [← nnreal.coe_le, ← nnreal.coe_le, nnreal.coe_sub h, nnreal.coe_add, sub_le_iff_le_add]
 | or.inr h :=
   have r ≤ p + q, from le_add_right h,
   by simpa [nnreal.coe_le, nnreal.coe_le, sub_eq_zero h]
@@ -359,7 +368,7 @@ lemma add_sub_cancel' {r p : nnreal} : (r + p) - r = p :=
 by rw [add_comm, add_sub_cancel]
 
 @[simp] lemma sub_add_cancel_of_le {a b : nnreal} (h : b ≤ a) : (a - b) + b = a :=
-nnreal.eq $ by rw [nnreal.coe_add, nnreal.coe_sub _ _ h, sub_add_cancel]
+nnreal.eq $ by rw [nnreal.coe_add, nnreal.coe_sub h, sub_add_cancel]
 
 end sub
 
@@ -395,10 +404,13 @@ by rw [← mul_le_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm
 @[simp] lemma lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : (r < p⁻¹ ↔ r * p < 1) :=
 by rw [← mul_lt_mul_left (zero_lt_iff_ne_zero.2 h), mul_inv_cancel h, mul_comm]
 
-lemma mul_le_if_le_inv {a b r : nnreal} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b :=
+lemma mul_le_iff_le_inv {a b r : ℝ≥0} (hr : r ≠ 0) : r * a ≤ b ↔ a ≤ r⁻¹ * b :=
 have 0 < r, from lt_of_le_of_ne (zero_le r) hr.symm,
 by rw [← @mul_le_mul_left _ _ a _ r this, ← mul_assoc, mul_inv_cancel hr, one_mul]
 
+lemma le_div_iff_mul_le {a b r : ℝ≥0} (hr : r ≠ 0) : a ≤ b / r ↔ a * r ≤ b :=
+by rw [div_def, mul_comm, ← mul_le_iff_le_inv hr, mul_comm]
+
 lemma le_of_forall_lt_one_mul_lt {x y : ℝ≥0} (h : ∀a<1, a * x ≤ y) : x ≤ y :=
 le_of_forall_ge_of_dense $ assume a ha,
   have hx : x ≠ 0 := zero_lt_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha),

src/order/filter/basic.lean

@@ -1578,6 +1578,10 @@ lemma tendsto_at_top_at_top_of_monotone [nonempty α] [semilattice_sup α] [preo
 
 alias tendsto_at_top_at_top_of_monotone ← monotone.tendsto_at_top_at_top
 
+lemma tendsto_finset_range : tendsto finset.range at_top at_top :=
+(tendsto_at_top_at_top _).2 (λ s, ⟨s.sup id + 1, λ N hN n hn,
+  finset.mem_range.2 $ lt_of_le_of_lt (finset.le_sup hn) $ nat.lt_of_succ_le hN⟩)
+
 lemma tendsto_finset_image_at_top_at_top {i : β → γ} {j : γ → β} (h : ∀x, j (i x) = x) :
   tendsto (λs:finset γ, s.image j) at_top at_top :=
 tendsto_infi.2 $ assume s, tendsto_infi' (s.image i) $ tendsto_principal_principal.2 $

src/topology/algebra/infinite_sum.lean

@@ -124,11 +124,7 @@ show tendsto (λs:finset β, s.sum (g ∘ f)) at_top (𝓝 (g a)),
 /-- If `f : ℕ → α` has sum `a`, then the partial sums `∑_{i=0}^{n-1} f i` converge to `a`. -/
 lemma tendsto_sum_nat_of_has_sum {f : ℕ → α} (h : has_sum f a) :
   tendsto (λn:ℕ, (range n).sum f) at_top (𝓝 a) :=
-suffices map (λ (n : ℕ), sum (range n) f) at_top ≤ map (λ (s : finset ℕ), sum s f) at_top,
-  from le_trans this h,
-assume s (hs : {t : finset ℕ | t.sum f ∈ s} ∈ at_top),
-let ⟨t, ht⟩ := mem_at_top_sets.mp hs, ⟨n, hn⟩ := @exists_nat_subset_range t in
-mem_at_top_sets.mpr ⟨n, assume n' hn', ht _ $ finset.subset.trans hn $ range_subset.mpr hn'⟩
+@tendsto.comp _ _ _ finset.range (λ s : finset ℕ, s.sum f) _ _ _ h tendsto_finset_range
 
 variable [topological_add_monoid α]
 
@@ -490,15 +486,8 @@ end
 
 lemma sum_le_has_sum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : has_sum f a) :
   s.sum f ≤ a :=
-let f' := λ b, if b ∈ s then f b else 0 in
-have hf' : has_sum f' (s.sum f'),
-  from has_sum_sum_of_ne_finset_zero $ λ b hb, if_neg hb,
-have hle : ∀ b, f' b ≤ f b,
-  from λ b, if hb : b ∈ s
-    then by simp only [f', if_pos hb]
-    else by simp only [f', if_neg hb, hs b hb],
-calc s.sum f = s.sum f' : finset.sum_congr rfl $ λ b hb, (if_pos hb).symm
-... ≤ a : has_sum_le hle hf' hf
+ge_of_tendsto at_top_ne_bot hf (mem_at_top_sets.2 ⟨s, λ t hst,
+  sum_le_sum_of_subset_of_nonneg hst $ λ b hbt hbs, hs b hbs⟩)
 
 lemma sum_le_tsum {f : β → α} (s : finset β) (hs : ∀ b∉s, 0 ≤ f b) (hf : summable f) :
   s.sum f ≤ tsum f :=
@@ -582,22 +571,75 @@ end uniform_group
 section cauchy_seq
 open finset.Ico filter
 
+/-- If the extended distance between consequent points of a sequence is estimated
+by a summable series of `nnreal`s, then the original sequence is a Cauchy sequence. -/
+lemma cauchy_seq_of_edist_le_of_summable [emetric_space α] {f : ℕ → α} (d : ℕ → nnreal)
+  (hf : ∀ n, edist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
+begin
+  refine emetric.cauchy_seq_iff_nnreal.2 (λ ε εpos, _),
+  -- Actually we need partial sums of `d` to be a Cauchy sequence
+  replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
+    let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
+  -- Now we take the same `N` as in one of the definitions of a Cauchy sequence
+  refine (metric.cauchy_seq_iff'.1 hd ε (nnreal.coe_pos.2 εpos)).imp (λ N hN n hn, _),
+  have hsum := hN n hn,
+  -- We simplify the known inequality
+  rw [dist_nndist, nnreal.nndist_eq, ← sum_range_add_sum_Ico _ hn, nnreal.add_sub_cancel'] at hsum,
+  norm_cast at hsum,
+  replace hsum := lt_of_le_of_lt (le_max_left _ _) hsum,
+
+  -- Then use `hf` to simplify the goal to the same form
+  apply lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn (λ k _ _, hf k)),
+  assumption_mod_cast
+end
+
+/-- If the distance between consequent points of a sequence is estimated by a summable series,
+then the original sequence is a Cauchy sequence. -/
+lemma cauchy_seq_of_dist_le_of_summable [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
+  (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) : cauchy_seq f :=
+begin
+  refine metric.cauchy_seq_iff'.2 (λε εpos, _),
+  replace hd : cauchy_seq (λ (n : ℕ), sum (range n) d) :=
+    let ⟨_, H⟩ := hd in cauchy_seq_of_tendsto_nhds _ (tendsto_sum_nat_of_has_sum H),
+  refine (metric.cauchy_seq_iff'.1 hd ε εpos).imp (λ N hN n hn, _),
+  have hsum := hN n hn,
+  rw [real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum,
+  calc dist (f n) (f N) = dist (f N) (f n) : dist_comm _ _
+  ... ≤ (Ico N n).sum d : dist_le_Ico_sum_of_dist_le hn (λ k _ _, hf k)
+  ... ≤ abs ((Ico N n).sum d) : le_abs_self _
+  ... < ε : hsum
+end
+
 lemma cauchy_seq_of_summable_dist [metric_space α] {f : ℕ → α}
   (h : summable (λn, dist (f n) (f n.succ))) : cauchy_seq f :=
+cauchy_seq_of_dist_le_of_summable _ (λ _, le_refl _) h
+
+lemma dist_le_tsum_of_dist_le_of_tendsto [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
+  (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a))
+  (n : ℕ) :
+  dist (f n) a ≤ ∑ m, d (n + m) :=
 begin
-  let d := λn, dist (f n) (f (n+1)),
-  refine metric.cauchy_seq_iff'.2 (λε εpos, _),
-  rcases (summable_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, _⟩,
-  calc dist (f n) (f N) ≤ (Ico N n).sum d : by rw dist_comm; apply dist_le_Ico_sum_dist f 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)))
+  refine le_of_tendsto at_top_ne_bot (tendsto_dist tendsto_const_nhds ha)
+    (mem_at_top_sets.2 ⟨n, λ m hnm, _⟩),
+  refine le_trans (dist_le_Ico_sum_of_dist_le hnm (λ k _ _, hf k)) _,
+  rw [sum_Ico_eq_sum_range],
+  refine sum_le_tsum (range _) (λ _ _, le_trans dist_nonneg (hf _)) _,
+  exact summable_comp_of_summable_of_injective _ hd (add_left_injective n)
 end
 
+lemma dist_le_tsum_of_dist_le_of_tendsto₀ [metric_space α] {f : ℕ → α} (d : ℕ → ℝ)
+  (hf : ∀ n, dist (f n) (f n.succ) ≤ d n) (hd : summable d) {a : α} (ha : tendsto f at_top (𝓝 a)) :
+  dist (f 0) a ≤ tsum d :=
+by simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0
+
+lemma dist_le_tsum_dist_of_tendsto [metric_space α] {f : ℕ → α}
+  (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) (n) :
+  dist (f n) a ≤ ∑ m, dist (f (n+m)) (f (n+m).succ) :=
+dist_le_tsum_of_dist_le_of_tendsto (λ n, dist (f n) (f n.succ)) (λ _, le_refl _) h ha n
+
+lemma dist_le_tsum_dist_of_tendsto₀ [metric_space α] {f : ℕ → α}
+  (h : summable (λn, dist (f n) (f n.succ))) {a : α} (ha : tendsto f at_top (𝓝 a)) :
+  dist (f 0) a ≤ ∑ n, dist (f n) (f n.succ) :=
+by simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0
+
 end cauchy_seq

src/topology/metric_space/basic.lean

@@ -767,6 +767,19 @@ section nnreal
 
 instance : metric_space nnreal := by unfold nnreal; apply_instance
 
+lemma nnreal.dist_eq (a b : nnreal) : dist a b = abs ((a:ℝ) - b) := rfl
+
+lemma nnreal.nndist_eq (a b : nnreal) :
+  nndist a b = max (a - b) (b - a) :=
+begin
+  wlog h : a ≤ b,
+  { apply nnreal.coe_eq.1,
+    rw [nnreal.sub_eq_zero h, max_eq_right (zero_le $ b - a), ← dist_nndist, nnreal.dist_eq,
+      nnreal.coe_sub h, abs, neg_sub],
+    apply max_eq_right,
+    linarith [nnreal.coe_le.2 h] },
+  rwa [nndist_comm, max_comm]
+end
 end nnreal
 
 section prod

src/topology/metric_space/emetric_space.lean

@@ -559,6 +559,25 @@ begin
                     ... = ε : ennreal.add_halves _⟩ }
 end
 
+/-- A variation of the emetric characterization of Cauchy sequences that deals with
+`nnreal` upper bounds. -/
+theorem cauchy_seq_iff_nnreal [inhabited β] [semilattice_sup β] {u : β → α} :
+  cauchy_seq u ↔ ∀ ε : nnreal, 0 < ε → ∃ N, ∀ n, N ≤ n → edist (u N) (u n) < ε :=
+begin
+  refine cauchy_seq_iff'.trans
+    ⟨λ H ε εpos, (H ε (ennreal.coe_pos.2 εpos)).imp $
+      λ N hN n hn, edist_comm (u n) (u N) ▸ hN n hn,
+      λ H ε εpos, _⟩,
+  specialize H ((min 1 ε).to_nnreal)
+    (ennreal.to_nnreal_pos_iff.2 ⟨lt_min ennreal.zero_lt_one εpos,
+      ennreal.lt_top_iff_ne_top.1 $ min_lt_iff.2 $ or.inl ennreal.coe_lt_top⟩),
+  refine H.imp (λ N hN n hn, edist_comm (u N) (u n) ▸ lt_of_lt_of_le (hN n hn) _),
+  refine ennreal.coe_le_iff.2 _,
+  rintros ε rfl,
+  rw [← ennreal.coe_one, ← ennreal.coe_min, ennreal.to_nnreal_coe],
+  apply min_le_right
+end
+
 theorem totally_bounded_iff {s : set α} :
   totally_bounded s ↔ ∀ ε > 0, ∃t : set α, finite t ∧ s ⊆ ⋃y∈t, ball y ε :=
 ⟨λ H ε ε0, H _ (edist_mem_uniformity ε0),

src/topology/uniform_space/cauchy.lean

@@ -113,6 +113,11 @@ defined on ℝ is Cauchy at +∞ to deduce convergence. Therefore, we define it
 is general enough to cover both ℕ and ℝ, which are the main motivating examples. -/
 def cauchy_seq [semilattice_sup β] (u : β → α) := cauchy (at_top.map u)
 
+lemma cauchy_seq_of_tendsto_nhds [semilattice_sup β] [nonempty β] (f : β → α) {x}
+  (hx : tendsto f at_top (𝓝 x)) :
+  cauchy_seq f :=
+cauchy_downwards cauchy_nhds (map_ne_bot at_top_ne_bot) hx
+
 lemma cauchy_seq_iff_prod_map [inhabited β] [semilattice_sup β] {u : β → α} :
   cauchy_seq u ↔ map (prod.map u u) at_top ≤ 𝓤 α :=
 iff.trans (and_iff_right (map_ne_bot at_top_ne_bot)) (prod_map_at_top_eq u u ▸ iff.rfl)