tendsto_sum_nat_add — Mathlib

English

For f: ℕ → ℝ≥0∞, Tendsto of the shifted tsum to 0 holds under non-top conditions.

Русский

Для f: ℕ → ℝ≥0∞ существует предел нуль для сдвинутой суммы.

LaTeX

$$$\\\\forall f : \\\\mathbb{N} \\\\to \\\\mathbb{R}_{\\\\ge 0}\\\\infty, \\\\mathrm{Tendsto}(n \\mapsto \\\\sum' k, f(k+n)) atTop (\\\\mathcal{N}(0))$$$

Lean4

theorem tendsto_sum_nat_add (f : ℕ → ℝ≥0∞) (hf : ∑' i, f i ≠ ∞) : Tendsto (fun i => ∑' k, f (k + i)) atTop (𝓝 0) :=
  by
  lift f to ℕ → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
  replace hf : Summable f := tsum_coe_ne_top_iff_summable.1 hf
  simp only [← ENNReal.coe_tsum, NNReal.summable_nat_add _ hf, ← ENNReal.coe_zero]
  exact mod_cast NNReal.tendsto_sum_nat_add f

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