English
Let f: N → α be a sequence in a seminormed additive group such that HasSum f a. If there exist real C and r with r < 1 and ∥f(n)∥ ≤ C · r^n for all n, then the partial sums converge to a with a geometric rate: ∥(∑_{k=0}^{n-1} f(k)) − a∥ ≤ C · r^n / (1 − r) for all n.
Русский
Пусть f: N → α — последовательность в полугруппе с нормой, имеющая сумму a. Если существуют вещественные C и r с r < 1 и ∥f(n)∥ ≤ C · r^n для всех n, тогда частичные суммы сходятся к a с геометрической скоростью: ∥(∑_{k=0}^{n-1} f(k)) − a∥ ≤ C · r^n / (1 − r) для всех n.
LaTeX
$$$\forall {\alpha} [\text{SeminormedAddCommGroup } \alpha] \; {f : \mathbb{N} \to \alpha} {a : \alpha} {C : \mathbb{R}} {r : \mathbb{R}}\, (hr : r < 1) (hf : \forall n, \|f(n)\| \le C \cdot r^n) \; HasSum f a \; \Longrightarrow \\ \forall n, \|\Big(\sum_{k=0}^{n-1} f(k)\Big) - a\| \le C \cdot r^n / (1 - r) $$$
Lean4
/-- If `‖f n‖ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` are within
distance `C * r ^ n / (1 - r)` of the sum of the series. This lemma does not assume `0 ≤ r` or
`0 ≤ C`. -/
theorem norm_sub_le_of_geometric_bound_of_hasSum (hr : r < 1) (hf : ∀ n, ‖f n‖ ≤ C * r ^ n) {a : α} (ha : HasSum f a)
(n : ℕ) : ‖(∑ x ∈ Finset.range n, f x) - a‖ ≤ C * r ^ n / (1 - r) :=
by
rw [← dist_eq_norm]
apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf)
exact ha.tendsto_sum_nat
