liouvilleNumber — Mathlib

English

Liouville's constant is the series LiouvilleNumber(m) = sum_{i≥0} 1/m^{i!}. It converges for m>1; for m≤1, the sum is defined to be 0.

Русский

Константа Лиувилля задаётся как сумма ряда LiouvilleNumber(m) = ∑_{i≥0} 1/m^{i!}. Ряд сходится при m>1, иначе сумма равна 0.

LaTeX

$$$\\mathrm{LiouvilleNumber}(m)=\\sum_{i=0}^{\\infty} m^{-i!}$ with convergence for $m>1$, otherwise 0.$$

Lean4

/-- For a real number `m`, Liouville's constant is
$$
\sum_{i=0}^\infty\frac{1}{m^{i!}}.
$$
The series converges only for `1 < m`. However, there is no restriction on `m`, since,
if the series does not converge, then the sum of the series is defined to be zero.
-/
def liouvilleNumber (m : ℝ) : ℝ :=
  ∑' i : ℕ, 1 / m ^ i !

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