English
For rational ξ and q with |ξ−q| less than 1/(q.den)^2, one gets bounds on q.den and q.num in terms of ξ.den.
Русский
Для рационального ξ и q при |ξ−q|<1/(q.den)^2 выполняются ограничения на q.den и q.num в зависимости от ξ.den.
LaTeX
$$$$|ξ-q|<1/(q.den)^2 \\Rightarrow q.den \\le ξ.den \\wedge ⌈ξ q.den⌉-1 \\le q.num \\le ⌊ξ q.den⌋+1.$$$$
Lean4
/-- If `ξ` is rational, then the good rational approximations to `ξ` have bounded
numerator and denominator. -/
theorem den_le_and_le_num_le_of_sub_lt_one_div_den_sq {ξ q : ℚ} (h : |ξ - q| < 1 / (q.den : ℚ) ^ 2) :
q.den ≤ ξ.den ∧ ⌈ξ * q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * q.den⌋ + 1 :=
by
have hq₀ : (0 : ℚ) < q.den := Nat.cast_pos.mpr q.pos
replace h : |ξ * q.den - q.num| < 1 / q.den :=
by
rw [← mul_lt_mul_iff_left₀ hq₀] at h
conv_lhs at h => rw [← abs_of_pos hq₀, ← abs_mul, sub_mul, mul_den_eq_num]
rwa [sq, div_mul, mul_div_cancel_left₀ _ hq₀.ne'] at h
constructor
· rcases eq_or_ne ξ q with (rfl | H)
· exact le_rfl
· have hξ₀ : (0 : ℚ) < ξ.den := Nat.cast_pos.mpr ξ.pos
rw [← Rat.num_div_den ξ, div_mul_eq_mul_div, div_sub' hξ₀.ne', abs_div, abs_of_pos hξ₀, div_lt_iff₀ hξ₀,
div_mul_comm, mul_one] at h
refine Nat.cast_le.mp ((one_lt_div hq₀).mp <| lt_of_le_of_lt ?_ h).le
norm_cast
rw [mul_comm _ q.num]
exact Int.one_le_abs (sub_ne_zero_of_ne <| mt Rat.eq_iff_mul_eq_mul.mpr H)
· obtain ⟨h₁, h₂⟩ :=
abs_sub_lt_iff.mp
(h.trans_le <| (one_div_le zero_lt_one hq₀).mp <| (@one_div_one ℚ _).symm ▸ Nat.cast_le.mpr q.pos)
rw [sub_lt_iff_lt_add, add_comm] at h₁ h₂
rw [← sub_lt_iff_lt_add] at h₂
norm_cast at h₁ h₂
exact ⟨sub_le_iff_le_add.mpr (Int.ceil_le.mpr h₁.le), sub_le_iff_le_add.mp (Int.le_floor.mpr h₂.le)⟩
