English
Let ξ be a real number and q a rational number with |ξ − q| < 1/(2·(den(q))^2). Then q is a convergent of the continued fraction expansion of ξ.
Русский
Пусть ξ — действительное число, q — рациональное число и выполняется неравенство |ξ − q| < 1/(2·(den(q))^2). Тогда q является конвергентом непрерывного дробного разложения ξ.
LaTeX
$$$|\\xi - q| < \\dfrac{1}{2 \\bigl(\\operatorname{den}(q)\\bigr)^2} \\implies \\exists n \\in \\mathbb{N}, (\\mathrm{GenContFract.of}\\ \\xi).convs\\ n = q$$$
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 is the version using `GenContFract.convs`. -/
theorem exists_convs_eq_rat {q : ℚ} (h : |ξ - q| < 1 / (2 * (q.den : ℝ) ^ 2)) : ∃ n, (GenContFract.of ξ).convs n = q :=
by
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h
exact ⟨n, hn.symm ▸ convs_eq_convergent ξ n⟩
