Theorems · Theorem · sequences and series

cauchySeq_finset_of_geometric_bound

∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α},
  r < 1 → (∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) → CauchySeq fun s => ∑ x ∈ s, f x

If ‖f n‖ ≤ C * r ^ n for all n : ℕ and some r < 1, then the partial sums of f form a Cauchy sequence. This lemma does not assume 0 ≤ r or 0 ≤ C.

Defined in

Mathlib.Analysis.SpecificLimits.Normed

Cited by

1 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroup