Diophantine Approximation #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 natural0 < n, there are integersjandkwith0 < k ≤ nand|k*ξ - j| ≤ 1/(n+1),real.exists_nat_abs_mul_sub_round_le, which replacesjbyround(k*ξ)and uses a natural numberk,real.exists_rat_abs_sub_le_and_denom_le, which says that there is a rational numberqsatisfying|ξ - q| ≤ 1/((n+1)*q.denom)andq.denom ≤ n,
and
real.infinite_rat_abs_sub_lt_one_div_denom_sq_of_irrational, which states that for irrationalξ, the set{q : ℚ | |ξ - q| < 1/q.denom^2}is infinite.
We also show a converse,
rat.finite_rat_abs_sub_lt_one_div_denom_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_denom_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
generalized_continued_fraction.convergents of generalized_continued_fraction.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.denom ≤ n and |ξ - q| ≤ 1/((n+1)*q.denom).
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.denom ≤ n and |ξ - q| ≤ 1/((n+1)*q.denom).
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.
Given any rational approximation q to the irrational real number ξ, there is
a good rational approximation q' such that |ξ - q'| < |ξ - q|.
Finitely many good approximations to rational numbers #
We now show that a rational number ξ has only finitely many good rational
approximations.
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
(generalized_continued_fraction.of ξ).convergents and
(generalized_continued_fraction.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 ξ.)
The zeroth convergent of ξ is ⌊ξ⌋.
The (n+1)th convergent of ξ is the nth convergent of 1/(fract ξ).
All convergents of 0 are zero.
If ξ is an integer, all its convergents equal ξ.
Our convergents agree with generalized_continued_fraction.convergents.
The nth convergent of the generalized_continued_fraction.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.denom^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.denom^2),
then q is a convergent of the continued fraction expansion of ξ.
This is the version using generalized_contined_fraction.convergents.