# Documentation

Mathlib.NumberTheory.DiophantineApproximation

# Diophantine Approximation #

The first part of this file gives proofs of various versions of Dirichlet's approximation theorem and its important consequence that when $\xi$ is an irrational real number, then there are infinitely many rationals $x/y$ (in lowest terms) such that $$\left|\xi - \frac{x}{y}\right| < \frac{1}{y^2} ,.$$ The proof is based on the pigeonhole principle.

The second part of the file gives a proof of Legendre's Theorem on rational approximation, which states that if $\xi$ is a real number and $x/y$ is a rational number such that $$\left|\xi - \frac{x}{y}\right| < \frac{1}{2y^2} ,,$$ then $x/y$ must be a convergent of the continued fraction expansion of $\xi$.

## Main statements #

The main results are three variants of Dirichlet's approximation theorem:

• Real.exists_int_int_abs_mul_sub_le, which states that for all real ξ and natural 0 < n, there are integers j and k with 0 < k ≤ n and |k*ξ - j| ≤ 1/(n+1),
• Real.exists_nat_abs_mul_sub_round_le, which replaces j by round(k*ξ) and uses a natural number k,
• Real.exists_rat_abs_sub_le_and_den_le, which says that there is a rational number q satisfying |ξ - q| ≤ 1/((n+1)*q.den) and q.den ≤ n,

and

• Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational, which states that for irrational ξ, the set {q : ℚ | |ξ - q| < 1/q.den^2} is infinite.

We also show a converse,

• Rat.finite_rat_abs_sub_lt_one_div_den_sq, which states that the set above is finite when ξ is a rational number.

Both statements are combined to give an equivalence, Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational.

There are two versions of Legendre's Theorem. One, Real.exists_rat_eq_convergent, uses Real.convergent, a simple recursive definition of the convergents that is also defined in this file, whereas the other, Real.exists_continued_fraction_convergent_eq_rat, uses GeneralizedContinuedFraction.convergents of GeneralizedContinuedFraction.of ξ.

## Implementation notes #

We use the namespace Real for the results on real numbers and Rat for the results on rational numbers. We introduce a secondary namespace real.contfrac_legendre to separate off a definition and some technical auxiliary lemmas used in the proof of Legendre's Theorem. For remarks on the proof of Legendre's Theorem, see below.

https://en.wikipedia.org/wiki/Dirichlet%27s_approximation_theorem https://de.wikipedia.org/wiki/Kettenbruch (The German Wikipedia page on continued fractions is much more extensive than the English one.)

## Tags #

Diophantine approximation, Dirichlet's approximation theorem, continued fraction