English
For m ∈ ℕ with hm > 0 and any k ∈ ℕ, there exists p ∈ ℕ such that partialSum m k = p / (m^k!): the k-th partial sum is a rational with denominator m^k!.
Русский
Для m ∈ ℕ с hm > 0 и любого k ∈ ℕ существует p ∈ ℕ такое, что partialSum m k = p / (m^k !): k-я частичная сумма рациональна с знаменателем m^k!.
LaTeX
$${hm > 0} ⇒ ∃ p ∈ ℕ, partialSum m k = p / (m^{k!})$$
Lean4
/-- The sum of the `k` initial terms of the Liouville number to base `m` is a ratio of natural
numbers where the denominator is `m ^ k!`. -/
theorem partialSum_eq_rat {m : ℕ} (hm : 0 < m) (k : ℕ) : ∃ p : ℕ, partialSum m k = p / ((m ^ k ! :) : ℝ) := by
induction k with
| zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial, pow_one, pow_one]⟩
| succ k h =>
rcases h with ⟨p_k, h_k⟩
use p_k * m ^ ((k + 1)! - k !) + 1
rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
· norm_cast
rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
simp [mul_assoc]
all_goals positivity
