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) : 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 n.succ)) : CauchySeq f

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 : ℕ) => ∑ i ∈ Finset.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 : ℕ) => ∑ i ∈ Finset.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 ι), ∑ x ∈ u, f x ≤ c) : Summable f

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

theorem Real.tsum_le_of_sum_range_le {f : ℕ → ℝ} {c : ℝ} (hf : ∀ (n : ℕ), 0 ≤ f n) (h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) : ∑' (n : ℕ), f n ≤ c

theorem Summable.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.

@[deprecated Summable.tsum_lt_tsum_of_nonneg (since := "2025-04-12")]

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

Alias of Summable.tsum_lt_tsum_of_nonneg.

---

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.