cauchy_series_of_le_geometric' — Mathlib

English

If h: ∥u(n)∥ ≤ C r^n holds for all n, then the partial sums ∑_{k< n} u(k) form a Cauchy sequence.

Русский

Если выполняется ∥u(n)∥ ≤ C r^n для всех n, то частичные суммы образуют последовательность Коши.

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)\| ≤ 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 + 1), u k :=
  (cauchy_series_of_le_geometric hr h).comp_tendsto <| tendsto_add_atTop_nat 1

Похожие утверждения