liouville_liouvilleNumber — Mathlib

English

For m ≥ 2, the Liouville number liouvilleNumber m.cast is indeed a Liouville number.

Русский

Для m ≥ 2 число Лиувиля liouvilleNumber m.cast действительно является числом Лиувиля.

LaTeX

$$$ \forall m \in \mathbb N,\ 2 \le m \Rightarrow \Liouville(\liouvilleNumber m.cast)$$$

Lean4

theorem liouville_liouvilleNumber {m : ℕ} (hm : 2 ≤ m) : Liouville (liouvilleNumber m) := by
  -- two useful inequalities

  have mZ1 : 1 < (m : ℤ) := by norm_cast
  have m1 : 1 < (m : ℝ) := by norm_cast
  intro n
  rcases partialSum_eq_rat (zero_lt_two.trans_le hm) n with ⟨p, hp⟩
  refine ⟨p, m ^ n !, one_lt_pow₀ mZ1 n.factorial_ne_zero, ?_⟩
  push_cast
  rw [Nat.cast_pow] at hp
  rw [← partialSum_add_remainder m1 n, ← hp]
  have hpos := remainder_pos m1 n
  simpa [abs_of_pos hpos, hpos.ne'] using @remainder_lt n m (by assumption_mod_cast)

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