English
A rational number has only finitely many good rational approximations.
Русский
У рационального числа имеется лишь конечное число хороших рациональных приближений.
LaTeX
$$$$\\{ q∈\\mathbb{Q} : |ξ-q| < 1/(q.den)^2 \\} \\text{ is finite. }$$$$
Lean4
/-- A rational number has only finitely many good rational approximations. -/
theorem finite_rat_abs_sub_lt_one_div_den_sq (ξ : ℚ) : {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}.Finite :=
by
let f : ℚ → ℤ × ℕ := fun q => (q.num, q.den)
set s := {q : ℚ | |ξ - q| < 1 / (q.den : ℚ) ^ 2}
have hinj : Function.Injective f := by
intro a b hab
simp only [f, Prod.mk_inj] at hab
rw [← Rat.num_div_den a, ← Rat.num_div_den b, hab.1, hab.2]
have H : f '' s ⊆ ⋃ (y : ℕ) (_ : y ∈ Ioc 0 ξ.den), Icc (⌈ξ * y⌉ - 1) (⌊ξ * y⌋ + 1) ×ˢ { y } :=
by
intro xy hxy
simp only [mem_image] at hxy
obtain ⟨q, hq₁, hq₂⟩ := hxy
obtain ⟨hd, hn⟩ := den_le_and_le_num_le_of_sub_lt_one_div_den_sq hq₁
simp_rw [mem_iUnion]
refine ⟨q.den, Set.mem_Ioc.mpr ⟨q.pos, hd⟩, ?_⟩
simp only [prod_singleton, mem_image, mem_Icc]
exact ⟨q.num, hn, hq₂⟩
refine (Finite.subset ?_ H).of_finite_image hinj.injOn
exact Finite.biUnion (finite_Ioc _ _) fun x _ => Finite.prod (finite_Icc _ _) (finite_singleton _)
