Infinite sum in the reals

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

theorem cauchySeq_of_edist_le_of_summable {α : Type u_1} [PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → NNReal) (hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)) (hd : Summable d) : CauchySeq f

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 cauchySeq_of_dist_le_of_summable {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ) (hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n) (hd : Summable d) : CauchySeq f

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

theorem cauchySeq_of_summable_dist {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} (h : Summable fun (n : ℕ) => dist (f n) (f (Nat.succ n))) : CauchySeq f

theorem dist_le_tsum_of_dist_le_of_tendsto {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ) (hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n) (hd : Summable d) {a : α} (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

theorem dist_le_tsum_of_dist_le_of_tendsto₀ {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} {a : α} (d : ℕ → ℝ) (hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n) (hd : Summable d) (ha : Filter.Tendsto f Filter.atTop (nhds a)) : dist (f 0) a ≤ tsum d

theorem dist_le_tsum_dist_of_tendsto {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} {a : α} (h : Summable fun (n : ℕ) => dist (f n) (f (Nat.succ n))) (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ℕ) : dist (f n) a ≤ ∑' (m : ℕ), dist (f (n + m)) (f (Nat.succ (n + m)))

theorem dist_le_tsum_dist_of_tendsto₀ {α : Type u_1} [PseudoMetricSpace α] {f : ℕ → α} {a : α} (h : Summable fun (n : ℕ) => dist (f n) (f (Nat.succ n))) (ha : Filter.Tendsto f Filter.atTop (nhds a)) : dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f (Nat.succ n))