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_convs_eq_rat defined in the file Mathlib.NumberTheory.DiophantineApproximation.ContinuedFraction, uses GenContFract.convs of GenContFract.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).

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_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : ∃ (q : ℚ), |ξ - ↑q| ≤ 1 / ((↑n + 1) * ↑q.den) ∧ q.den ≤ n

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.

theorem Real.exists_rat_abs_sub_lt_and_lt_of_irrational {ξ : ℝ} (hξ : Irrational ξ) (q : ℚ) : ∃ (q' : ℚ), |ξ - ↑q'| < 1 / ↑q'.den ^ 2 ∧ |ξ - ↑q'| < |ξ - ↑q|

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

theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational {ξ : ℝ} (hξ : Irrational ξ) : {q : ℚ | |ξ - ↑q| < 1 / ↑q.den ^ 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.

theorem Rat.den_le_and_le_num_le_of_sub_lt_one_div_den_sq {ξ q : ℚ} (h : |ξ - q| < 1 / ↑q.den ^ 2) : q.den ≤ ξ.den ∧ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

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

theorem Rat.finite_rat_abs_sub_lt_one_div_den_sq (ξ : ℚ) : {q : ℚ | |ξ - q| < 1 / ↑q.den ^ 2}.Finite

A rational number has only finitely many good rational approximations.

theorem Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational (ξ : ℝ) : {q : ℚ | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ

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

noncomputable def Real.convergent : ℝ → ℕ → ℚ

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 (GenContFract.of ξ).convs and (GenContFract.of ξ).convs' 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.convs_eq_convergent. (Note that we use the fact that 1/0 = 0 here to make it work for rational ξ.)

Equations

• x✝.convergent 0 = ↑⌊x✝⌋
• x✝.convergent n.succ = ↑⌊x✝⌋ + ((Int.fract x✝)⁻¹.convergent n)⁻¹

@[simp]

theorem Real.convergent_zero (ξ : ℝ) : ξ.convergent 0 = ↑⌊ξ⌋

The zeroth convergent of ξ is ⌊ξ⌋.

@[simp]

theorem Real.convergent_succ (ξ : ℝ) (n : ℕ) : ξ.convergent (n + 1) = ↑⌊ξ⌋ + ((Int.fract ξ)⁻¹.convergent n)⁻¹

The (n+1)th convergent of ξ is the nth convergent of 1/(fract ξ).

@[simp]

theorem Real.convergent_of_zero (n : ℕ) : Real.convergent 0 n = 0

All convergents of 0 are zero.

@[simp]

theorem Real.convergent_of_int {ξ : ℤ} (n : ℕ) : (↑ξ).convergent n = ↑ξ

If ξ is an integer, all its convergents equal ξ.

The key technical condition for the induction proof

def Real.ContfracLegendre.Ass (ξ : ℝ) (u v : ℤ) : Prop

Define the technical condition to be used as assumption in the inductive proof.

Equations

• Real.ContfracLegendre.Ass ξ u v = (IsCoprime u v ∧ (v = 1 → -(1 / 2) < ξ - ↑u) ∧ |ξ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹)

The main result

theorem Real.exists_rat_eq_convergent' {ξ : ℝ} {u : ℤ} {v : ℕ} (h : Real.ContfracLegendre.Ass ξ u ↑v) : ∃ (n : ℕ), ↑u / ↑v = ξ.convergent n

The technical version of Legendre's Theorem.

theorem Real.exists_rat_eq_convergent {ξ : ℝ} {q : ℚ} (h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)) : ∃ (n : ℕ), q = ξ.convergent n

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.