Thue's gap principle and Thue's approximation theorem

Let α be an algebraic number of degree d ≥ 2 and let κ > d / 2 + 1. Thue's gap principle says that a good rational approximation ξ₁ of α, that is |ξ₁ - α| ≤ H(ξ₁) ^ (-κ), of large height controls the heights of all other good approximations: there are constants C and λ, depending only on α and κ, such that H(ξ₁) ≥ C implies H(ξ) ≤ H(ξ₁) ^ λ for every ξ ∈ ℚ with |ξ - α| ≤ H(ξ) ^ (-κ). Here H is the multiplicative height Height.mulHeight₁ on ℚ. Only the existence of C and λ is stated, not Evertse's explicit values.

By Northcott's theorem there are only finitely many rationals of bounded height, so the gap principle gives Thue's approximation theorem: |ξ - α| ≤ H(ξ) ^ (-κ) has only finitely many rational solutions ξ.

Main results

• TauCeti.thue_gap_principle: Thue's gap principle, for complex algebraic α.
• TauCeti.thue_approximation: Thue's approximation theorem, for complex algebraic α.
• TauCeti.thue_approximation_real: Thue's approximation theorem for real algebraic α.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Theorems 6.9 and 6.14.

theorem TauCeti.thue_gap_principle {α : ℂ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ} (hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) : ∃ (C : ℝ) (lam : ℝ), 1 ≤ C ∧ 1 ≤ lam ∧ ∀ (ξ₁ ξ : ℚ), ‖↑ξ₁ - α‖ ≤ Height.mulHeight₁ ξ₁ ^ (-κ) → C ≤ Height.mulHeight₁ ξ₁ → ‖↑ξ - α‖ ≤ Height.mulHeight₁ ξ ^ (-κ) → Height.mulHeight₁ ξ ≤ Height.mulHeight₁ ξ₁ ^ lam

Thue's gap principle (Evertse, Theorem 6.14). Let α be a complex algebraic number of degree d ≥ 2 and let κ > d / 2 + 1. There are constants C ≥ 1 and λ ≥ 1 such that for all rationals ξ₁ and ξ with |ξ₁ - α| ≤ H(ξ₁) ^ (-κ), H(ξ₁) ≥ C and |ξ - α| ≤ H(ξ) ^ (-κ), the heights satisfy H(ξ) ≤ H(ξ₁) ^ λ. The degree hypothesis already forces α to be algebraic.

theorem TauCeti.thue_approximation {α : ℂ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ} (hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) : {ξ : ℚ | ‖↑ξ - α‖ ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite

Thue's approximation theorem, for complex α. Let α be a complex algebraic number of degree d ≥ 2 and let κ > d / 2 + 1. Then only finitely many rationals ξ satisfy |ξ - α| ≤ H(ξ) ^ (-κ). This is a variant of Evertse, Theorem 6.9, rather than that statement verbatim: here α may be complex and every degree d ≥ 2 is allowed.

theorem TauCeti.thue_approximation_real {α : ℝ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ} (hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) : {ξ : ℚ | |↑ξ - α| ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite

Thue's approximation theorem for real α. Let α be a real algebraic number of degree d ≥ 2 and let κ > d / 2 + 1. Then only finitely many rationals ξ satisfy |ξ - α| ≤ H(ξ) ^ (-κ). This is a variant of Evertse, Theorem 6.9, rather than that statement verbatim: every degree d ≥ 2 is allowed.