hasSum_nat_add_iff — Mathlib

English

HasSum for a shifted sequence relates to HasSum for the original sequence via the initial finite block: HasSum(f(n+k)) a iff HasSum f (a + ∑_{i<k} f(i)).

Русский

HasSum для сдвинутой последовательности связана с HasSum для исходной через сумму первых k членов: HasSum(f(n+k)) a эквивалентно HasSum f (a + ∑_{i<k} f(i)).

LaTeX

$$HasSum(f(n+k)) a ↔ HasSum f (a + ∑_{i∈range k} f(i))$$

Lean4

nonrec theorem hasSum_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) {a : ℝ≥0} :
    HasSum (fun n => f (n + k)) a ↔ HasSum f (a + ∑ i ∈ range k, f i) := by
  rw [← hasSum_coe, hasSum_nat_add_iff (f := fun n => toReal (f n)) k]; norm_cast

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