Badly approximable numbers and Littlewood's conjecture

A real number ξ is badly approximable if it is irrational and there is c > 0 with q ‖q ξ‖ ≥ c for every integer q ≥ 1, where ‖x‖ = |x - round x| is the distance to the nearest integer. Equivalently, |ξ - r| ≥ c / den(r) ^ 2 for every rational r (badlyApproximable_iff_forall_ratCast), so for a fixed badly approximable ξ the constant in Dirichlet's bound |ξ - p / q| < 1 / q ^ 2 cannot be made arbitrarily small. Badly approximable numbers have irrationality exponent exactly 2 (BadlyApproximable.irrationalityExponent_eq), so they are not Liouville numbers, and one-dimensional simultaneous exponent exactly 1 (BadlyApproximable.simultaneousExponent_eq_one). The property is invariant under the rational affine maps ξ ↦ ξ + r and ξ ↦ r ξ with r ≠ 0. Liouville's inequality makes every real quadratic irrational badly approximable (badlyApproximable_of_natDegree_minpoly_eq_two); in particular √2 is (badlyApproximable_sqrt_two).

Littlewood's conjecture asserts that inf_{y ≥ 1} y ‖y α‖ ‖y β‖ = 0 for all real α, β. It is open, and is recorded here only as the proposition LittlewoodConjecture. It holds for α, β as soon as one of them is not badly approximable (littlewood_of_not_badlyApproximable), so it reduces to pairs of badly approximable numbers (littlewoodConjecture_iff_badlyApproximable). Dirichlet's theorem in nearest-integer form (Real.infinite_setOf_mul_abs_mul_sub_round_le_one) gives the weaker unconditional statement that y ‖y α‖ ‖y β‖ ≤ 1 for infinitely many y ≥ 1 (Real.infinite_setOf_mul_le_one).

Main definitions

• TauCeti.BadlyApproximable ξ: ξ is irrational and q ‖q ξ‖ is bounded below by a positive constant for q ≥ 1.
• TauCeti.LittlewoodConjecture: Littlewood's conjecture, as a proposition.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), Chapter 2, §2.2, Exercises 2.6 and 2.7 and p. 23.

def TauCeti.BadlyApproximable (ξ : ℝ) : Prop

A real number ξ is badly approximable if it is irrational and there is a constant c > 0 with c ≤ q ‖q ξ‖ for every natural number q ≥ 1, where ‖x‖ = |x - round x| is the distance from x to the nearest integer.

theorem TauCeti.badlyApproximable_iff {ξ : ℝ} : BadlyApproximable ξ ↔ ∃ c > 0, ∀ (q : ℕ), 0 < q → c ≤ ↑q * |↑q * ξ - ↑(round (↑q * ξ))|

The irrationality condition in BadlyApproximable is automatic: ξ is badly approximable exactly when q ‖q ξ‖ is bounded below by a positive constant for q ≥ 1.

theorem TauCeti.BadlyApproximable.irrational {ξ : ℝ} (h : BadlyApproximable ξ) : Irrational ξ

A badly approximable number is irrational.

@[simp]

theorem Rat.not_badlyApproximable (r : ℚ) : ¬TauCeti.BadlyApproximable ↑r

A rational number is not badly approximable.

theorem TauCeti.badlyApproximable_iff_forall_ratCast {ξ : ℝ} : BadlyApproximable ξ ↔ ∃ c > 0, ∀ (r : ℚ), c / ↑r.den ^ 2 ≤ |ξ - ↑r|

ξ is badly approximable exactly when there is c > 0 such that every rational number r satisfies |ξ - r| ≥ c / den(r) ^ 2.

theorem TauCeti.BadlyApproximable.not_liouvilleWith {ξ p : ℝ} (h : BadlyApproximable ξ) (hp : 2 < p) : ¬LiouvilleWith p ξ

A badly approximable number is not a Liouville number with any exponent p > 2.

theorem TauCeti.BadlyApproximable.irrationalityExponent_eq {ξ : ℝ} (h : BadlyApproximable ξ) : irrationalityExponent ξ = 2

A badly approximable number has irrationality exponent 2.

theorem TauCeti.BadlyApproximable.simultaneousExponent_eq_one {ξ : ℝ} (h : BadlyApproximable ξ) : simultaneousExponent ![ξ] = 1

A badly approximable number has one-dimensional simultaneous exponent 1.

theorem TauCeti.BadlyApproximable.not_liouville {ξ : ℝ} (h : BadlyApproximable ξ) : ¬Liouville ξ

A badly approximable number is not a Liouville number.

theorem TauCeti.BadlyApproximable.add_ratCast {ξ : ℝ} (h : BadlyApproximable ξ) (s : ℚ) : BadlyApproximable (ξ + ↑s)

Adding a rational number preserves bad approximability.

theorem TauCeti.BadlyApproximable.ratCast_mul {ξ : ℝ} (h : BadlyApproximable ξ) {s : ℚ} (hs : s ≠ 0) : BadlyApproximable (↑s * ξ)

Multiplying by a nonzero rational number preserves bad approximability.

@[simp]

theorem TauCeti.badlyApproximable_add_ratCast_iff {ξ : ℝ} {s : ℚ} : BadlyApproximable (ξ + ↑s) ↔ BadlyApproximable ξ

Adding a rational number does not change bad approximability.

@[simp]

theorem TauCeti.badlyApproximable_ratCast_mul_iff {ξ : ℝ} {s : ℚ} (hs : s ≠ 0) : BadlyApproximable (↑s * ξ) ↔ BadlyApproximable ξ

Multiplying by a nonzero rational number does not change bad approximability.

@[simp]

theorem TauCeti.badlyApproximable_neg_iff {ξ : ℝ} : BadlyApproximable (-ξ) ↔ BadlyApproximable ξ

Negation does not change bad approximability.

Quadratic irrationals

theorem Irrational.badlyApproximable_of_aeval_eq_zero {ξ : ℝ} (hξ : Irrational ξ) {f : Polynomial ℤ} (hf : f ≠ 0) (hdeg : f.natDegree ≤ 2) (hroot : (Polynomial.aeval ξ) f = 0) : TauCeti.BadlyApproximable ξ

Liouville's theorem in degree two. An irrational root of a nonzero integer polynomial of degree at most 2 is badly approximable.

theorem TauCeti.badlyApproximable_of_natDegree_minpoly_eq_two {ξ : ℝ} (h : (minpoly ℚ ξ).natDegree = 2) : BadlyApproximable ξ

Liouville's theorem in degree two. A real number whose minimal polynomial over ℚ has degree 2 is badly approximable.

theorem TauCeti.badlyApproximable_sqrt_two : BadlyApproximable √2

√2 is badly approximable.

Littlewood's conjecture

def TauCeti.LittlewoodConjecture : Prop

Littlewood's conjecture: for all real α, β and every ε > 0 there is y ≥ 1 with y ‖y α‖ ‖y β‖ < ε, where ‖x‖ = |x - round x|. This is an open problem; it is recorded as a proposition to be used as an explicit hypothesis.

theorem TauCeti.littlewoodConjecture_def : LittlewoodConjecture ↔ ∀ (α β ε : ℝ), ε > 0 → ∃ (y : ℕ), 0 < y ∧ ↑y * |↑y * α - ↑(round (↑y * α))| * |↑y * β - ↑(round (↑y * β))| < ε

The quantified formulation of Littlewood's conjecture.

theorem TauCeti.littlewood_of_not_badlyApproximable {α : ℝ} (hα : ¬BadlyApproximable α) (β : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (y : ℕ), 0 < y ∧ ↑y * |↑y * α - ↑(round (↑y * α))| * |↑y * β - ↑(round (↑y * β))| < ε

Littlewood's conjecture holds for a pair (α, β) as soon as α is not badly approximable.

theorem TauCeti.littlewoodConjecture_iff_badlyApproximable : LittlewoodConjecture ↔ ∀ (α β : ℝ), BadlyApproximable α → BadlyApproximable β → ∀ ε > 0, ∃ (y : ℕ), 0 < y ∧ ↑y * |↑y * α - ↑(round (↑y * α))| * |↑y * β - ↑(round (↑y * β))| < ε

Littlewood's conjecture reduces to pairs of badly approximable numbers.

Examples