Restatements of results from Diophantine Approximation using Mathlib.Algebra.ContinuedFractions. #
Main statements #
There are two versions of Legendre's Theorem.
Real.exists_rat_eq_convergent, defined in Mathlib.NumberTheory.DiophantineApproximation.Basic,
uses Real.convergent, a simple recursive definition of the convergents that is also defined
in that file. This file provides Real.exists_convs_eq_rat, using
GenContFract.convs of GenContFract.of ξ.
Our convergents agree with GenContFract.convs.
The nth convergent of the GenContFract.of ξ agrees with ξ.convergent n.
theorem
Real.exists_convs_eq_rat
{ξ : ℝ}
{q : ℚ}
(h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2))
:
∃ (n : ℕ), (GenContFract.of ξ).convs n = ↑q
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.