tsum_le_of_sum_range_le — Mathlib

English

If partial sums are all ≤ c, then the total sum is ≤ c.

Русский

Если частичные суммы не превосходят c, то сумма по всей области не превышает c.

LaTeX

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

Lean4

theorem tsum_le_of_sum_range_le {f : ℕ → ℝ≥0} {c : ℝ≥0} (h : ∀ n, ∑ i ∈ Finset.range n, f i ≤ c) : ∑' n, f n ≤ c :=
  (summable_of_sum_range_le h).tsum_le_of_sum_range_le h

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