English
If |ξ−q| < 1/(2 q.den^2), then q is a convergent of ξ.
Русский
Если |ξ−q| < 1/(2 q.den^2), то q является конвергентом ξ.
LaTeX
$$$$|\\xi - q| < \\frac{1}{2(q.den)^2} \\Rightarrow q = \\xi.convergent n\\text{ for some } n.$$$$
Lean4
/-- The main result, *Legendre's Theorem* on rational approximation:
if `ξ` is a real number and `q` is a rational number such that `|ξ - q| < 1/(2*q.den^2)`,
then `q` is a convergent of the continued fraction expansion of `ξ`.
This version uses `Real.convergent`. -/
theorem exists_rat_eq_convergent {q : ℚ} (h : |ξ - q| < 1 / (2 * (q.den : ℝ) ^ 2)) : ∃ n, q = ξ.convergent n :=
by
refine q.num_div_den ▸ exists_rat_eq_convergent' ⟨?_, fun hd => ?_, ?_⟩
· exact isCoprime_iff_nat_coprime.mpr (natAbs_natCast q.den ▸ q.reduced)
· rw [← q.den_eq_one_iff.mp (Nat.cast_eq_one.mp hd)] at h
simpa only [Rat.den_intCast, Nat.cast_one, one_pow, mul_one] using (abs_lt.mp h).1
· obtain ⟨hq₀, hq₁⟩ := aux₀ (Nat.cast_pos.mpr q.pos)
replace hq₁ := mul_pos hq₀ hq₁
have hq₂ : (0 : ℝ) < 2 * (q.den * q.den) := mul_pos zero_lt_two (mul_pos hq₀ hq₀)
rw [cast_natCast] at *
rw [(by norm_cast : (q.num / q.den : ℝ) = (q.num / q.den : ℚ)), Rat.num_div_den]
exact h.trans (by rw [← one_div, sq, one_div_lt_one_div hq₂ hq₁, ← sub_pos]; ring_nf; exact hq₀)
