tendsto_sum_nat_add — Mathlib

English

For any f: ℕ → ℝ≥0, the sums ∑' k, f(k+i) tend to 0 as i → ∞.

Русский

Для любой f: ℕ → ℝ≥0, суммы ∑' k, f(k+i) стремятся к 0 при i → ∞.

LaTeX

$$$\\\\mathrm{Tendsto}\\left(i \\mapsto \\\\sum' k, f(k+i)\\\\right) atTop (\\\\mathcal{N}(0))$$$

Lean4

/-- For `f : ℕ → ℝ≥0`, then `∑' k, f (k + i)` tends to zero. This does not require a summability
assumption on `f`, as otherwise all sums are zero. -/
theorem tendsto_sum_nat_add (f : ℕ → ℝ≥0) : Tendsto (fun i => ∑' k, f (k + i)) atTop (𝓝 0) :=
  by
  rw [← tendsto_coe]
  convert _root_.tendsto_sum_nat_add fun i => (f i : ℝ)
  norm_cast

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