remainder_pos

Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

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

← MathLib Explorer

English

If m>1, then the tail remainder is strictly positive for any k.

Русский

Если m>1, то остаток хвоста положителен для любого k.

LaTeX

$$$\\forall m>1,\\; \\forall k,\\; 0<\\mathrm{remainder}(m,k)$$$

Lean4

theorem remainder_pos {m : ℝ} (hm : 1 < m) (k : ℕ) : 0 < remainder m k :=
  (remainder_summable hm k).tsum_pos (fun _ => by positivity) 0 (by positivity)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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