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

theorem not_summable_iff_tendsto_nat_atTop_of_nonneg {f : ℕ → ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) : ¬Summable f ↔ Filter.Tendsto (fun (n : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => 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 : ℕ) => Finset.sum (Finset.range n) fun (i : ℕ) => f i) Filter.atTop Filter.atTop

theorem summable_sigma_of_nonneg {α : Type u_1} {β : α → Type u_3} {f : (x : α) × β x → ℝ} (hf : ∀ (x : (x : α) × β x), 0 ≤ f x) : Summable f ↔ (∀ (x : α), Summable fun (y : β x) => f { fst := x, snd := y }) ∧ Summable fun (x : α) => ∑' (y : β x), f { fst := x, snd := y }

theorem summable_prod_of_nonneg {α : Type u_1} {β : Type u_2} {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 ι), (Finset.sum u fun (x : ι) => f x) ≤ c) : Summable f

theorem summable_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (n : ℕ), (Finset.sum (Finset.range n) fun (i : ℕ) => f i) ≤ c) : Summable f

theorem Real.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (n : ℕ), (Finset.sum (Finset.range n) fun (i : ℕ) => 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.