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)