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}
[pseudo_emetric_space α]
{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}
[pseudo_metric_space α]
{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}
[pseudo_metric_space α]
{f : ℕ → α}
(h : summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ))) :
theorem
dist_le_tsum_of_dist_le_of_tendsto
{α : Type u_1}
[pseudo_metric_space α]
{f : ℕ → α}
(d : ℕ → ℝ)
(hf : ∀ (n : ℕ), has_dist.dist (f n) (f n.succ) ≤ d n)
(hd : summable d)
{a : α}
(ha : filter.tendsto f filter.at_top (nhds a))
(n : ℕ) :
theorem
dist_le_tsum_of_dist_le_of_tendsto₀
{α : Type u_1}
[pseudo_metric_space α]
{f : ℕ → α}
{a : α}
(d : ℕ → ℝ)
(hf : ∀ (n : ℕ), has_dist.dist (f n) (f n.succ) ≤ d n)
(hd : summable d)
(ha : filter.tendsto f filter.at_top (nhds a)) :
has_dist.dist (f 0) a ≤ tsum d
theorem
dist_le_tsum_dist_of_tendsto
{α : Type u_1}
[pseudo_metric_space α]
{f : ℕ → α}
{a : α}
(h : summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ)))
(ha : filter.tendsto f filter.at_top (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}
[pseudo_metric_space α]
{f : ℕ → α}
{a : α}
(h : summable (λ (n : ℕ), has_dist.dist (f n) (f n.succ)))
(ha : filter.tendsto f filter.at_top (nhds a)) :
has_dist.dist (f 0) a ≤ ∑' (n : ℕ), has_dist.dist (f n) (f n.succ)