# 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.

## References #

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

### Dirichlet's approximation theorem #

We show that for any real number `ξ`

and positive natural `n`

, there is a fraction `q`

such that `q.den ≤ n`

and `|ξ - q| ≤ 1/((n+1)*q.den)`

.

*Dirichlet's approximation theorem:*
For any real number `ξ`

and positive natural `n`

, there are integers `j`

and `k`

,
with `0 < k ≤ n`

and `|k*ξ - j| ≤ 1/(n+1)`

.

See also `Real.exists_nat_abs_mul_sub_round_le`

.

*Dirichlet's approximation theorem:*
For any real number `ξ`

and positive natural `n`

, there is a natural number `k`

,
with `0 < k ≤ n`

such that `|k*ξ - round(k*ξ)| ≤ 1/(n+1)`

.

*Dirichlet's approximation theorem:*
For any real number `ξ`

and positive natural `n`

, there is a fraction `q`

such that `q.den ≤ n`

and `|ξ - q| ≤ 1/((n+1)*q.den)`

.

See also `AddCircle.exists_norm_nsmul_le`

.

### Infinitely many good approximations to irrational numbers #

We show that an irrational real number `ξ`

has infinitely many "good rational approximations",
i.e., fractions `x/y`

in lowest terms such that `|ξ - x/y| < 1/y^2`

.

If `ξ`

is an irrational real number, then there are infinitely many good
rational approximations to `ξ`

.

### Finitely many good approximations to rational numbers #

We now show that a rational number `ξ`

has only finitely many good rational
approximations.

A rational number has only finitely many good rational approximations.

The set of good rational approximations to a real number `ξ`

is infinite if and only if
`ξ`

is irrational.

### Legendre's Theorem on Rational Approximation #

We prove **Legendre's Theorem** on rational approximation: If $\xi$ is a real number and
$x/y$ is a rational number such that $|\xi - x/y| < 1/(2y^2)$,
then $x/y$ is a convergent of the continued fraction expansion of $\xi$.

The proof is by induction. However, the induction proof does not work with the statement as given, since the assumption is too weak to imply the corresponding statement for the application of the induction hypothesis. This can be remedied by making the statement slightly stronger. Namely, we assume that $|\xi - x/y| < 1/(y(2y-1))$ when $y \ge 2$ and $-\frac{1}{2} < \xi - x < 1$ when $y = 1$.

### Convergents: definition and API lemmas #

We give a direct recursive definition of the convergents of the continued fraction
expansion of a real number `ξ`

. The main reason for that is that we want to have the
convergents as rational numbers; the versions
`(GeneralizedContinuedFraction.of ξ).convergents`

and
`(GeneralizedContinuedFraction.of ξ).convergents'`

always give something of the
same type as `ξ`

. We can then also use dot notation `ξ.convergent n`

.
Another minor reason is that this demonstrates that the proof
of Legendre's theorem does not need anything beyond this definition.
We provide a proof that this definition agrees with the other one;
see `Real.continued_fraction_convergent_eq_convergent`

.
(Note that we use the fact that `1/0 = 0`

here to make it work for rational `ξ`

.)

## Equations

- Real.convergent x 0 = ↑⌊x⌋
- Real.convergent x (Nat.succ n) = ↑⌊x⌋ + (Real.convergent (Int.fract x)⁻¹ n)⁻¹

## Instances For

The zeroth convergent of `ξ`

is `⌊ξ⌋`

.

The `(n+1)`

th convergent of `ξ`

is the `n`

th convergent of `1/(fract ξ)`

.

All convergents of `0`

are zero.

If `ξ`

is an integer, all its convergents equal `ξ`

.

Our `convergent`

s agree with `GeneralizedContinuedFraction.convergents`

.

The `n`

th convergent of the `GeneralizedContinuedFraction.of ξ`

agrees with `ξ.convergent n`

.

### The key technical condition for the induction proof #

### The main result #

The technical version of *Legendre's Theorem*.

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`

.

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 `generalized_contined_fraction.convergents`

.