remainder — Mathlib

English

The remainder from k+1 onward is the tail sum of Liouville's constant: sum_{i=k+1}^∞ 1/m^{i!}.

Русский

Остаток для индекса k+1 — это сумма хвоста константы Лиувилля: сумма от i=k+1 до бесконечности 1/m^{i!}.

LaTeX

$$$\\mathrm{remainder}(m,k)=\\sum_{i= k+1}^{\\infty} m^{-i!}$$$

Lean4

/-- `LiouvilleNumber.remainder` is the sum of the series of the terms in `liouvilleNumber m`
starting from `k+1`, i.e
$$
\sum_{i=k+1}^\infty\frac{1}{m^{i!}}.
$$
-/
def remainder (m : ℝ) (k : ℕ) : ℝ :=
  ∑' i, 1 / m ^ (i + (k + 1))!

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