summable_nat_add_iff — Mathlib

English

For all k, the shifted sequence f(n+k) is summable if and only if f is summable.

Русский

Для любого k сумма f(n+k) суммируема тогда и только тогда, когда суммируема f.

LaTeX

$$Summable(f) ↔ Summable( n ↦ f(n+k) )$$

Lean4

nonrec theorem summable_nat_add_iff {f : ℕ → ℝ≥0} (k : ℕ) : (Summable fun i => f (i + k)) ↔ Summable f :=
  by
  rw [← summable_coe, ← summable_coe]
  exact @summable_nat_add_iff ℝ _ _ _ (fun i => (f i : ℝ)) k

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