remainder_summable — Mathlib

English

For any m>1, the tail sums remain summable after shifting by k+1; i.e., the tail starting at k+1 is summable.

Русский

Для любого m>1 хвостовой ряд, начиная с k+1, также сходится.

LaTeX

$$$\\forall m>1,\\; \\mathrm{remainder}(m, k)\\text{ is Summable as a tail()}$$$

Lean4

theorem remainder_summable {m : ℝ} (hm : 1 < m) (k : ℕ) : Summable fun i : ℕ => 1 / m ^ (i + (k + 1))! := by
  convert (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)

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