Documentation

Mathlib.Topology.Algebra.InfiniteSum.Real

Infinite sum in the reals #

This file provides lemmas about Cauchy sequences in terms of infinite sums and infinite sums valued in the reals.

theorem cauchySeq_of_dist_le_of_summable {α : Type u_1} [PseudoMetricSpace α] {f : α} (d : ) (hf : ∀ (n : ), 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 cauchySeq_of_summable_dist {α : Type u_1} [PseudoMetricSpace α] {f : α} (h : Summable fun (n : ) => dist (f n) (f n.succ)) :
theorem dist_le_tsum_of_dist_le_of_tendsto {α : Type u_1} [PseudoMetricSpace α] {f : α} (d : ) (hf : ∀ (n : ), dist (f n) (f n.succ) 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 n.succ) 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 n.succ)) (ha : Filter.Tendsto f Filter.atTop (nhds a)) (n : ) :
dist (f n) a ∑' (m : ), dist (f (n + m)) (f (n + m).succ)
theorem dist_le_tsum_dist_of_tendsto₀ {α : Type u_1} [PseudoMetricSpace α] {f : α} {a : α} (h : Summable fun (n : ) => dist (f n) (f n.succ)) (ha : Filter.Tendsto f Filter.atTop (nhds a)) :
dist (f 0) a ∑' (n : ), dist (f n) (f n.succ)
theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : } (hf : ∀ (n : ), 0 f n) :
¬Summable f Filter.Tendsto (fun (n : ) => iFinset.range n, f i) Filter.atTop Filter.atTop
theorem summable_iff_not_tendsto_nat_atTop_of_nonneg {f : } (hf : ∀ (n : ), 0 f n) :
Summable f ¬Filter.Tendsto (fun (n : ) => iFinset.range n, f i) Filter.atTop Filter.atTop
theorem summable_sigma_of_nonneg {α : Type u_4} {β : αType u_3} {f : (x : α) × β x} (hf : ∀ (x : (x : α) × β x), 0 f x) :
Summable f (∀ (x : α), Summable fun (y : β x) => f x, y) Summable fun (x : α) => ∑' (y : β x), f x, y
theorem summable_partition {α : Type u_3} {β : Type u_4} {f : β} (hf : 0 f) {s : αSet β} (hs : ∀ (i : β), ∃! j : α, i s j) :
Summable f (∀ (j : α), Summable fun (i : (s j)) => f i) Summable fun (j : α) => ∑' (i : (s j)), f i
theorem summable_prod_of_nonneg {α : Type u_3} {β : Type u_4} {f : α × β} (hf : 0 f) :
Summable f (∀ (x : α), Summable fun (y : β) => f (x, y)) Summable fun (x : α) => ∑' (y : β), f (x, y)
theorem summable_of_sum_le {ι : Type u_3} {f : ι} {c : } (hf : 0 f) (h : ∀ (u : Finset ι), xu, f x c) :
theorem summable_of_sum_range_le {f : } {c : } (hf : ∀ (n : ), 0 f n) (h : ∀ (n : ), iFinset.range n, f i c) :
theorem Real.tsum_le_of_sum_range_le {f : } {c : } (hf : ∀ (n : ), 0 f n) (h : ∀ (n : ), iFinset.range n, f i c) :
∑' (n : ), f n c
theorem tsum_lt_tsum_of_nonneg {i : } {f : } {g : } (h0 : ∀ (b : ), 0 f b) (h : ∀ (b : ), f b g b) (hi : f i < g i) (hg : Summable g) :
∑' (n : ), f n < ∑' (n : ), g n

If a sequence f with non-negative terms is dominated by a sequence g with summable series and at least one term of f is strictly smaller than the corresponding term in g, then the series of f is strictly smaller than the series of g.