mathlib documentation

number_theory.diophantine_approximation

Diophantine Approximation #

This file gives proofs of various versions of Dirichlet's approximation theorem and its important consequence that when ξ is an irrational real number, then there are infinitely many rationals x/y (in lowest terms) such that |ξ - x/y| < 1/y^2.

The proof is based on the pigeonhole principle.

Main statements #

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

and

We also show a converse,

Both statements are combined to give an equivalence, real.infinite_rat_abs_sub_lt_one_div_denom_sq_iff_irrational.

Implementation notes #

We use the namespace real for the results on real numbers and rat for the results on rational numbers.

References #

https://en.wikipedia.org/wiki/Dirichlet%27s_approximation_theorem

Tags #

Diophantine approximation, Dirichlet's approximation theorem

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

theorem real.exists_int_int_abs_mul_sub_le (ξ : ) {n : } (n_pos : 0 < n) :
(j k : ), 0 < k k n |k * ξ - j| 1 / (n + 1)

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.

theorem real.exists_nat_abs_mul_sub_round_le (ξ : ) {n : } (n_pos : 0 < n) :
(k : ), 0 < k k n |k * ξ - (round (k * ξ))| 1 / (n + 1)

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

theorem real.exists_rat_abs_sub_le_and_denom_le (ξ : ) {n : } (n_pos : 0 < n) :
(q : ), |ξ - q| 1 / ((n + 1) * (q.denom)) q.denom n

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.

theorem real.exists_rat_abs_sub_lt_and_lt_of_irrational {ξ : } (hξ : irrational ξ) (q : ) :
(q' : ), |ξ - q'| < 1 / (q'.denom) ^ 2 |ξ - q'| < |ξ - q|

Given any rational approximation q to the irrational real number ξ, there is a good rational approximation q' such that |ξ - q'| < |ξ - q|.

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.

theorem rat.denom_le_and_le_num_le_of_sub_lt_one_div_denom_sq {ξ q : } (h : |ξ - q| < 1 / (q.denom) ^ 2) :

If ξ is rational, then the good rational approximations to ξ have bounded numerator and denominator.

theorem rat.finite_rat_abs_sub_lt_one_div_denom_sq (ξ : ) :
{q : | |ξ - q| < 1 / (q.denom) ^ 2}.finite

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.