summable_nat_add — Mathlib

English

If a nonnegative sequence f on natural numbers is summable, then any tail f(i+k) is summable for any k.

Русский

Если последовательность f(n)≥0 на ℕ суммируема, то любая сдвинутая на k последовательность f(n+k) суммируема.

LaTeX

$$Summable(f) → ∀k, Summable( n ↦ f(n+k) )$$

Lean4

theorem summable_nat_add (f : ℕ → ℝ≥0) (hf : Summable f) (k : ℕ) : Summable fun i => f (i + k) :=
  summable_comp_injective hf <| add_left_injective k

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