English
If 0 < r < 1 and ∥u(n)∥ ≤ C r^n for all n, then the sequence of partial sums ∑_{k< n} u(k) is Cauchy, and moreover the same bound holds with a truncated head as in the previous lemma.
Русский
Если 0 < r < 1 и ∥u(n)∥ ≤ C r^n для всех n, то последовательность частичных сумм ∑_{k< n} u(k) является Коши; аналогично хвостовая форма сохраняет ограничение.
LaTeX
$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] (C \in \mathbb{R}) (u : \mathbb{N} \to \alpha) (N : \mathbb{N}) (r : \mathbb{R}) (hr0 : 0 < r) (hr1 : r < 1) (h : \forall n, \|u(n)\| ≤ C r^n) \\ → \\ CauchySeq (\lambda n, ∑_{k< n} u(k))$$$
Lean4
/-- The term norms of any convergent series are bounded by a constant. -/
theorem exists_norm_le_of_cauchySeq (h : CauchySeq fun n ↦ ∑ k ∈ range n, f k) : ∃ C, ∀ n, ‖f n‖ ≤ C :=
by
obtain ⟨b, ⟨_, key, _⟩⟩ := cauchySeq_iff_le_tendsto_0.mp h
refine ⟨b 0, fun n ↦ ?_⟩
simpa only [dist_partial_sum'] using key n (n + 1) 0 (_root_.zero_le _) (_root_.zero_le _)
