Documentation

Mathlib.Topology.Algebra.InfiniteSum.Real

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) :

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) :

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))) :
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))