English
For any x ∈ ℝ, LiouvilleWith 1 x holds; i.e., every real number is Liouville with exponent 1 (trivially).
Русский
Для всякого x ∈ ℝ верно LiouvilleWith 1 x; то есть любое вещественное число является Liouville с экспонентом 1 (тривиально).
LaTeX
$$$ \LiouvilleWith 1(x) $$$
Lean4
/-- For `p = 1` (hence, for any `p ≤ 1`), the condition `LiouvilleWith p x` is trivial. -/
theorem liouvilleWith_one (x : ℝ) : LiouvilleWith 1 x := by
use 2
refine ((eventually_gt_atTop 0).mono fun n hn => ?_).frequently
have hn' : (0 : ℝ) < n := by simpa
have : x < ↑(⌊x * ↑n⌋ + 1) / ↑n :=
by
rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]
exact Int.lt_floor_add_one _
refine ⟨⌊x * n⌋ + 1, this.ne, ?_⟩
rw [abs_sub_comm, abs_of_pos (sub_pos.2 this), rpow_one, sub_lt_iff_lt_add', add_div_eq_mul_add_div _ _ hn'.ne']
gcongr
calc
_ ≤ x * n + 1 := by push_cast; gcongr; apply Int.floor_le
_ < x * n + 2 := by linarith
