English
The product of a LiouvilleWith p x with an integer m ≠ 0 preserves LiouvilleWith p (m · x).
Русский
Произведение числа LiouvilleWith p x на целое m ≠ 0 сохраняет LiouvilleWith p (m · x).
LaTeX
$$$ LiouvilleWith p (m \cdot x) $$$
Lean4
/-- The product of a Liouville number and a nonzero rational number is again a Liouville number. -/
theorem mul_rat (h : LiouvilleWith p x) (hr : r ≠ 0) : LiouvilleWith p (x * r) :=
by
rcases h.exists_pos with ⟨C, _hC₀, hC⟩
refine ⟨r.den ^ p * (|r| * C), (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
rintro n ⟨_hn, m, hne, hlt⟩
have A : (↑(r.num * m) : ℝ) / ↑(r.den • id n) = m / n * r := by simp [← div_mul_div_comm, ← r.cast_def, mul_comm]
refine ⟨r.num * m, ?_, ?_⟩
· rw [A]; simp [hne, hr]
· rw [A, ← sub_mul, abs_mul]
simp only [smul_eq_mul, id, Nat.cast_mul]
calc
_ < C / ↑n ^ p * |↑r| := by gcongr
_ = ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p := ?_
rw [mul_rpow, mul_div_mul_left, mul_comm, mul_div_assoc]
· simp only [Rat.cast_abs]
all_goals positivity
