summable_of_sum_range_le — Mathlib

English

If for all n, the partial sums ∑_{i< n} f(i) are ≤ c, then f is summable.

Русский

Если частичные суммы ограничены сверху константой c, то функция суммируема.

LaTeX

$$$\\\\forall f : \\\\mathbb{N} \\rightarrow \\\\mathbb{R}_{\\\\ge 0}, \\\\forall c \\\\ge 0, \\\\big(\\\\forall n, \\\\sum_{i=0}^{n-1} f(i) \\\\le c\\\\big) \\\\Rightarrow \\\\mathrm{Summable}(f)$$$

Lean4

theorem summable_of_sum_range_le {f : ℕ → ℝ≥0} {c : ℝ≥0} (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : Summable f :=
  by
  refine summable_iff_not_tendsto_nat_atTop.2 fun H => ?_
  rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
  exact lt_irrefl _ (hn.trans_le (h n))

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