English
If x satisfies Liouville with exponent p > 2, then x (up to an integer shift) lies in a structured family of good rational approximants a/b with |x − a/b| < 1/b^(2+1/n) for some n > 0 and integers a, b with 0 ≤ a ≤ b.
Русский
Если x удовлетворяет условию Лиувиля с показателем p > 2, то после сдвига на целое число x находится внутри семейства хороших рациональных аппроксимантов a/b, таких что |x − a/b| < 1/b^(2+1/n) для некоторого n>0 и целых a, b с 0 ≤ a ≤ b.
LaTeX
$$$$ \{ x \in \mathbb{R} : \exists p>2, LiouvilleWith(p,x) \} \subseteq \bigcup_{m\in \mathbb{Z}} (\cdot + m)^{-1} \Big( \bigcup_{n>0} \{ x : \exists a \in \mathrm{Icc}(0,b), \exists b>0, |x - a/b| < 1/b^{2+1/n} \} \Big). $$$$
Lean4
theorem setOf_liouvilleWith_subset_aux :
{x : ℝ | ∃ p > 2, LiouvilleWith p x} ⊆
⋃ m : ℤ,
(· + (m : ℝ)) ⁻¹'
⋃ n > (0 : ℕ),
{x : ℝ |
∃ᶠ b : ℕ in atTop, ∃ a ∈ Finset.Icc (0 : ℤ) b, |x - (a : ℤ) / b| < 1 / (b : ℝ) ^ (2 + 1 / n : ℝ)} :=
by
rintro x ⟨p, hp, hxp⟩
rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
rw [lt_sub_iff_add_lt'] at hn
suffices
∀ y : ℝ,
LiouvilleWith p y →
y ∈ Ico (0 : ℝ) 1 →
∃ᶠ b : ℕ in atTop, ∃ a ∈ Finset.Icc (0 : ℤ) b, |y - a / b| < 1 / (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ)
by
simp only [mem_iUnion, mem_preimage]
have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico,
Int.cast_neg, le_add_neg_iff_add_le]
exact ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
clear hxp x; intro x hxp hx01
refine ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono ?_
rintro b ⟨⟨a, -, hlt⟩, hb⟩
rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt
refine ⟨a, ?_, hlt⟩
replace hb : (1 : ℝ) ≤ b := Nat.one_le_cast.2 hb
have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
replace hlt : |x - a / b| < 1 / b :=
by
refine hlt.trans_le (one_div_le_one_div_of_le hb0 ?_)
calc
(b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
_ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) := rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
simpa using n.cast_add_one_pos.le
rw [sub_div' hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_iff_of_pos_right hb0, abs_sub_lt_iff, sub_lt_iff_lt_add,
sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt
rw [Finset.mem_Icc, ← Int.lt_add_one_iff, ← Int.lt_add_one_iff, ← neg_lt_iff_pos_add, add_comm, ← @Int.cast_lt ℝ, ←
@Int.cast_lt ℝ]
push_cast
refine ⟨lt_of_le_of_lt ?_ hlt.1, hlt.2.trans_le ?_⟩
· simp only [mul_nonneg hx01.left b.cast_nonneg, neg_le_sub_iff_le_add, le_add_iff_nonneg_left]
· rw [add_le_add_iff_left]
exact mul_le_of_le_one_left hb0.le hx01.2.le
