Diophantine Approximation using continued fractions

Main statements

There are two versions of Legendre's Theorem.Real.exists_rat_eq_convergent, defined in Mathlib/NumberTheory/DiophantineApproximation/Basic.lean, 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.

theorem Real.convs_eq_convergent (ξ : ℝ) (n : ℕ) : (GenContFract.of ξ).convs n = ↑(ξ.convergent n)

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.