tsum_le_of_sum_range_le — Mathlib

English

If a nonnegative sequence has all partial sums bounded by c, then its total sum is ≤ c.

Русский

Если неотрицательная последовательность имеет все частичные суммы ≤ c, то суммарный ряд ≤ c.

LaTeX

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

Lean4

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

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