summable

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

URI: https://scilib.ai/kg/mathlib#LiouvilleNumber.summable

English

For m>1, the series ∑ 1/m^{i!} is summable; i.e., the Liouville constant converges.

Русский

При m>1 ряд ∑ 1/m^{i!} сходится; константа Лиувиля сходится.

LaTeX

$$$\\sum_{i=0}^{\\infty} m^{-i!} \\text{ summable for } m>1$$$

Lean4

protected theorem summable {m : ℝ} (hm : 1 < m) : Summable fun i : ℕ => 1 / m ^ i ! :=
  summable_one_div_pow_of_le hm Nat.self_le_factorial

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru