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 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_denom_le, which says that there is a rational number q satisfying |ξ - q| ≤ 1/((n+1)*q.denom) and q.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).

source

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

source

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

source

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.

source

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

source

theorem real.infinite_rat_abs_sub_lt_one_div_denom_sq_of_irrational {ξ : ℝ} (hξ : irrational ξ) :

{q : ℚ | |ξ - ↑q| < 1 / ↑(q.denom) ^ 2}.infinite

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.

source

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

q.denom ≤ ξ.denom ∧ ⌈ξ * ↑(q.denom)⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑(q.denom)⌋ + 1

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

source

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.

source

theorem real.infinite_rat_abs_sub_lt_one_div_denom_sq_iff_irrational (ξ : ℝ) :

{q : ℚ | |ξ - ↑q| < 1 / ↑(q.denom) ^ 2}.infinite ↔ irrational ξ

The set of good rational approximations to a real number ξ is infinite if and only if ξ is irrational.