tsum_le_of_sum_range_le — Mathlib

English

If partial sums satisfy ∑ i< n f i ≤ c for all n, then ∑' n f n ≤ c.

Русский

Если частичные суммы удовлетворяют ∑_{i< n} f(i) ≤ c для всех n, то ∑' n f(n) ≤ c.

LaTeX

$$$\\\\forall f : \\\\mathbb{N} \\\\to \\\\mathbb{R}_{\\\\ge 0∞}, \\\\forall c \\\\in \\\\mathbb{R}_{\\\\ge 0∞}, \\\\Big(\\\\forall n, \\\\sum i \\\\in \\\\mathrm{range}(n) f(i) \\\\le c\\\\Big) \\\\Rightarrow \\\\sum' n, 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 :=
  ENNReal.summable.tsum_le_of_sum_range_le h

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