sum_add_tsum_nat_add — Mathlib

English

For a summable f: ℕ → ℝ≥0, the full sum equals the sum of the initial k terms plus the sum of the tail starting at k.

Русский

Для суммируемой f: ℕ → ℝ≥0 полная сумма равна сумме первых k членов плюс сумма хвоста начиная с k.

LaTeX

$$∑' i, f(i) = (∑ i∈range k, f(i)) + ∑' i, f(i+k)$$

Lean4

theorem sum_add_tsum_nat_add {f : ℕ → ℝ≥0} (k : ℕ) (hf : Summable f) :
    ∑' i, f i = (∑ i ∈ range k, f i) + ∑' i, f (i + k) :=
  (((summable_nat_add_iff k).2 hf).sum_add_tsum_nat_add').symm

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