Hurwitz's Theorem in Diophantine Approximation

This file proves Hurwitz's approximation theorem: if $\xi$ is an irrational real number, then there are infinitely many irreducible rationals $x/y$ such that $$\left|\xi - \frac{x}{y}\right| < \frac{1}{\sqrt{5}\,y^2} \,.$$

This strengthens the corresponding Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational (Dirichlet's Theorem) with constant $1$ proved in Mathlib/NumberTheory/DiophantineApproximation/Basic.lean. In fact the constant $\sqrt 5$ is best possible, with the golden ratio being a counterexample for larger constants.

The proof avoids continued fractions entirely, instead using Farey brackets, which are pairs of rationals $\frac{p}{q} < \xi < \frac{r}{s}$ with $qr - ps = 1$. We can show that at least one of $\frac{p}{q}$, $\frac{r}{s}$ and the mediant $\frac{p+r}{q+s}$ satisfies the bound, and by repeatedly constructing smaller intervals around $\xi$, infinitude is achieved.

Main definitions

• Real.Hurwitz.IsFarey, defining a Farey interval on 4 integers p, q, r, s such that 0 < q, s and p/q < ξ < r/s with q*r - p*s = 1.

• Real.Hurwitz.IsGoodApprox defines a good approximation as one satisfying the Hurwitz bound without using division for simplicity. It can be accessed using Real.Hurwitz.isGoodApprox_iff.

Main statements

• Real.infinite_rat_abs_sub_lt_one_div_sqrt_five_mul_den_sq_of_irrational, which states that for irrational ξ the set {q : ℚ | |ξ - q| < 1/(√5 * q.den^2)} is infinite.

Implementation notes

We use the namespace Real for the main result and a secondary namespace Real.Hurwitz for the technical auxiliary lemmas, and a further IsFarey namespace is used to contain theorems regarding Farey brackets and mediants, following the pattern of Real.ContfracLegendre in Mathlib/NumberTheory/DiophantineApproximation/Basic.lean.

Intermediate lemmas are stated in the division-free form |y*ξ - x| * y * √5 < 1 rather than |ξ - x/y| < 1/(√5*y^2), which is substantially easier to manipulate. The two are related by Real.Hurwitz.IsGoodApprox.abs_sub_div_lt.

References

• G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers
• https://en.wikipedia.org/wiki/Hurwitz%27s_theorem_(number_theory)

Tags

Diophantine approximation, Hurwitz's theorem, Farey sequence, Stern-Brocot tree, mediant

structure Real.Hurwitz.IsFarey (ξ : ℝ) (p q r s : ℤ) : Prop

IsFarey ξ p q r s means p/q < ξ < r/s with q * r - p * s = 1. The determinant/ unimodularity condition ensures the mediant (p + r) / (q + s) creates a valid interval with each endpoint.

• q_pos : 0 < q

  Left denominator is positive.

• s_pos : 0 < s

  Right denominator is positive.

• det : q * r - p * s = 1

  Unimodularity condition.

• left : ↑p / ↑q < ξ

  p / q is a lower bound for ξ.

• right : ξ < ↑r / ↑s

  r / s is an upper bound for ξ.

def Real.Hurwitz.IsGoodApprox (ξ : ℝ) (x y : ℤ) : Prop

Divisionless reformulation of Hurwitz bound |ξ - x / y| < 1 / (√5 * y ^ 2).

Equations

• Real.Hurwitz.IsGoodApprox ξ x y = (0 < y ∧ |↑y * ξ - ↑x| * ↑y * √5 < 1)

theorem Real.Hurwitz.isGoodApprox_iff {ξ : ℝ} {x y : ℤ} : IsGoodApprox ξ x y ↔ 0 < y ∧ |↑y * ξ - ↑x| * ↑y * √5 < 1

Unfolding lemma for IsGoodApprox.

Bridging IsGoodApprox to aux₀ hypotheses

Important contradiction

Mediant properties

Key step: one of three consecutive Farey endpoints is good

theorem Real.Hurwitz.IsFarey.isGoodApprox_or {ξ : ℝ} (hξ : Irrational ξ) {p q r s : ℤ} (h : IsFarey ξ p q r s) : IsGoodApprox ξ p q ∨ IsGoodApprox ξ r s ∨ IsGoodApprox ξ (p + r) (q + s)

If IsFarey ξ p q r s, then at least one of p/q, r/s, and the mediant (p + r)/(q + s) satisfies the Hurwitz bound.

theorem Real.Hurwitz.IsFarey.exists_isGoodApprox {ξ : ℝ} (hξ : Irrational ξ) {p q r s : ℤ} (h : IsFarey ξ p q r s) : ∃ (x : ℤ) (y : ℤ), IsGoodApprox ξ x y ∧ |ξ - ↑x / ↑y| < 1 / (↑q * ↑s)

If IsFarey ξ p q r s, then there exists a good approximation to ξ closer than the width of the bracket.

Generating brackets of arbitrarily large denominators

theorem Real.Hurwitz.exists_isFarey_large {ξ : ℝ} (hξ : Irrational ξ) (n : ℕ) : ∃ (p : ℤ) (q : ℤ) (r : ℤ) (s : ℤ), IsFarey ξ p q r s ∧ ↑n ≤ q + s

Farey brackets around ξ with arbitrarily large denominator sum q + s (and therefore arbitrarily small width) exist.

From ℤ to ℚ, and infinitude

theorem Real.Hurwitz.IsGoodApprox.abs_sub_div_lt {ξ : ℝ} {x y : ℤ} (hg : IsGoodApprox ξ x y) : |ξ - ↑x / ↑y| < 1 / (√5 * ↑y ^ 2)

A good approximation in the division-free sense satisfies the usual Hurwitz bound |ξ - x / y| < 1 / (√5 * y ^ 2).

theorem Real.Hurwitz.exists_rat_abs_sub_lt_one_div_sqrt_five_mul_den_sq_and_lt_of_irrational {ξ : ℝ} (hξ : Irrational ξ) (t : ℚ) : ∃ (t' : ℚ), |ξ - ↑t'| < 1 / (√5 * ↑t'.den ^ 2) ∧ |ξ - ↑t'| < |ξ - ↑t|

Given any rational t, there is a rational t' satisfying the Hurwitz bound that is strictly closer to ξ than t is.

theorem Real.infinite_rat_abs_sub_lt_one_div_sqrt_five_mul_den_sq_of_irrational {ξ : ℝ} (hξ : Irrational ξ) : {t : ℚ | |ξ - ↑t| < 1 / (√5 * ↑t.den ^ 2)}.Infinite

Hurwitz's theorem. For irrational ξ, the set {q : ℚ | |ξ - q| < 1 / (√5 * q.den ^ 2)} is infinite.