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:
real.exists_int_int_abs_mul_sub_le
, which states that for all realξ
and natural0 < n
, there are integersj
andk
with0 < k ≤ n
and|k*ξ - j| ≤ 1/(n+1)
,real.exists_nat_abs_mul_sub_round_le
, which replacesj
byround(k*ξ)
and uses a natural numberk
,real.exists_rat_abs_sub_le_and_denom_le
, which says that there is a rational numberq
satisfying|ξ - 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
.
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)
.
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.