# mathlib3documentation

topology.algebra.infinite_sum.real

# Infinite sum in the reals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides lemmas about Cauchy sequences in terms of infinite sums.

theorem cauchy_seq_of_edist_le_of_summable {α : Type u_1} {f : α} (d : nnreal) (hf : (n : ), has_edist.edist (f n) (f n.succ) (d n)) (hd : summable d) :

If the extended distance between consecutive points of a sequence is estimated by a summable series of nnreals, then the original sequence is a Cauchy sequence.

theorem cauchy_seq_of_dist_le_of_summable {α : Type u_1} {f : α} (d : ) (hf : (n : ), has_dist.dist (f n) (f n.succ) d n) (hd : summable d) :

If the distance between consecutive points of a sequence is estimated by a summable series, then the original sequence is a Cauchy sequence.

theorem cauchy_seq_of_summable_dist {α : Type u_1} {f : α} (h : summable (λ (n : ), has_dist.dist (f n) (f n.succ))) :
theorem dist_le_tsum_of_dist_le_of_tendsto {α : Type u_1} {f : α} (d : ) (hf : (n : ), has_dist.dist (f n) (f n.succ) d n) (hd : summable d) {a : α} (ha : (nhds a)) (n : ) :
has_dist.dist (f n) a ∑' (m : ), d (n + m)
theorem dist_le_tsum_of_dist_le_of_tendsto₀ {α : Type u_1} {f : α} {a : α} (d : ) (hf : (n : ), has_dist.dist (f n) (f n.succ) d n) (hd : summable d) (ha : (nhds a)) :
theorem dist_le_tsum_dist_of_tendsto {α : Type u_1} {f : α} {a : α} (h : summable (λ (n : ), has_dist.dist (f n) (f n.succ))) (ha : (nhds a)) (n : ) :
has_dist.dist (f n) a ∑' (m : ), has_dist.dist (f (n + m)) (f (n + m).succ)
theorem dist_le_tsum_dist_of_tendsto₀ {α : Type u_1} {f : α} {a : α} (h : summable (λ (n : ), has_dist.dist (f n) (f n.succ))) (ha : (nhds a)) :
has_dist.dist (f 0) a ∑' (n : ), has_dist.dist (f n) (f n.succ)