English
If the terms are uniformly bounded by a geometric bound with ratio r < 1, the partial sums form a Cauchy sequence: if ∥u(n)∥ ≤ C r^n for all n with r < 1, then the sequence of partial sums ∑_{k< n} u(k) is Cauchy.
Русский
Если члены ограничены геометрически, т. е. ∥u(n)∥ ≤ C r^n при любом n и r < 1, то частичные суммы образуют Коши-последовательность: ∑_{k< n} u(k) является Коши.
LaTeX
$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] (C \in \mathbb{R}) (u : \mathbb{N} \to \alpha) (r \in \mathbb{R}) (hr : r < 1) (h : \forall n, \|u(n)\| \le C \cdot r^n) \\ → \\ CauchySeq (\lambda n, (\sum_{k< n} u(k)))$$$
Lean4
theorem cauchy_series_of_le_geometric {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1) (h : ∀ n, ‖u n‖ ≤ C * r ^ n) :
CauchySeq fun n ↦ ∑ k ∈ range n, u k :=
cauchySeq_of_le_geometric r C hr (by simp [h])
