Roth's theorem

Roth's theorem (Roth, 1955): if α is a real algebraic number and κ > 2, then only finitely many rational numbers ξ satisfy |ξ - α| ≤ H(ξ) ^ (-κ), where H is the multiplicative height Height.mulHeight₁ on ℚ. Equivalently, there is a constant c > 0 with |ξ - α| ≥ c H(ξ) ^ (-κ) for every ξ ∈ ℚ with ξ ≠ α; for irrational α this holds for every ξ ∈ ℚ. The proof is ineffective: it gives neither a bound for the heights of the exceptional ξ nor a value of c. For rational α the statement also holds, and is elementary. The lower bound extends to complex algebraic α, since a non-real α stays at distance at least |im α| from ℚ.

As consequences, a real algebraic number is not a Liouville number with any exponent p > 2, so its irrationality exponent is at most 2, and exactly 2 if it is irrational.

The proof assembles the steps of the auxiliary polynomial method. Suppose that infinitely many ξ satisfy the inequality. Fix a small ε > 0 and a number n of variables with 2 d ≤ exp (ε² n / 2), where d is the degree of α.

• Choose good approximations β₀, β₁, … of α whose logarithmic heights h(βₖ) start above a large bound L and grow by a factor M at each step (Northcott.exists_seq_mem_lt).
• For D = h(β_{n-1}) / ε, the degree bounds rₖ = ⌊D / h(βₖ)⌋₊ satisfy rₖ h(βₖ) ≈ D, and Roth's auxiliary polynomial P ∈ ℤ[X₀, …, X_{n-1}] with these partial degrees has index at least (n / 2) (1 - ε) at the diagonal point (α, …, α) (TauCeti.exists_roth_auxiliary_polynomial).
• By Roth's lemma (TauCeti.weightedIndex_le_of_logHeight_le), the index of P at β = (β₀, …, β_{n-1}) is at most 5 n ε / 2; the parameters are chosen as in TauCeti.inv_mul_add_le_floor_div_mul.
• The key inequality (TauCeti.roth_key_inequality) then gives κ (1 - ε) (1 / 2 - 3 ε) ≤ 1 + C₂ / (n L), which fails for small ε and large L because κ > 2.

Main results

• IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg: Roth's theorem, the finiteness of the set of very good rational approximations of a real algebraic number.
• IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub: Roth's theorem as a lower bound for |ξ - α|, for ξ ≠ α.
• IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_norm_sub: the same lower bound for a complex algebraic number α.
• IsAlgebraic.not_liouvilleWith: a real algebraic number is not LiouvilleWith p for p > 2.
• IsAlgebraic.irrationalityExponent_le_two, IsAlgebraic.irrationalityExponent_eq_two: the irrationality exponent of a real algebraic number is at most 2, and equal to 2 if the number is irrational.

References

• K. F. Roth, Rational approximations to algebraic numbers, Mathematika 2 (1955), 1–20.
• L. Pottmeyer, Diophantine Approximation (2022), Theorem 3.0.1 and §3.5.
• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Theorem 6.2.

theorem IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg {α : ℝ} (hα : IsAlgebraic ℚ α) {κ : ℝ} (hκ : 2 < κ) : {ξ : ℚ | |↑ξ - α| ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite

Roth's theorem (Roth, 1955). If α is a real algebraic number and κ > 2, then only finitely many rational numbers ξ satisfy |ξ - α| ≤ H(ξ) ^ (-κ), where H is the multiplicative height on ℚ.

theorem IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub {α : ℝ} (hα : IsAlgebraic ℚ α) {κ : ℝ} (hκ : 2 < κ) : ∃ (c : ℝ), 0 < c ∧ ∀ (ξ : ℚ), ↑ξ ≠ α → c * Height.mulHeight₁ ξ ^ (-κ) ≤ |↑ξ - α|

Roth's theorem as a lower bound (Evertse, Theorem 6.2). If α is a real algebraic number and κ > 2, then there is c > 0 with c H(ξ) ^ (-κ) ≤ |ξ - α| for every ξ ∈ ℚ with ξ ≠ α. For irrational α the condition ξ ≠ α always holds, by Irrational.ne_rat.

theorem IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_norm_sub {α : ℂ} (hα : IsAlgebraic ℚ α) {κ : ℝ} (hκ : 2 < κ) : ∃ (c : ℝ), 0 < c ∧ ∀ (ξ : ℚ), ↑ξ ≠ α → c * Height.mulHeight₁ ξ ^ (-κ) ≤ ‖↑ξ - α‖

Roth's theorem for a complex algebraic number (Evertse, remarks after Theorem 6.2). If α ∈ ℂ is algebraic and κ > 2, then there is c > 0 with c H(ξ) ^ (-κ) ≤ ‖ξ - α‖ for every ξ ∈ ℚ with ξ ≠ α. For real α this is IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub; a non-real α is at distance at least |im α| from every rational number.

theorem IsAlgebraic.not_liouvilleWith {α : ℝ} (hα : IsAlgebraic ℚ α) {p : ℝ} (hp : 2 < p) : ¬LiouvilleWith p α

Roth's theorem in terms of Liouville exponents: a real algebraic number is not a Liouville number with any exponent p > 2.

theorem IsAlgebraic.irrationalityExponent_le_two {α : ℝ} (hα : IsAlgebraic ℚ α) : TauCeti.irrationalityExponent α ≤ 2

The irrationality exponent of a real algebraic number is at most two.

theorem IsAlgebraic.irrationalityExponent_eq_two {α : ℝ} (hα : IsAlgebraic ℚ α) (hirr : Irrational α) : TauCeti.irrationalityExponent α = 2

The irrationality exponent of a real algebraic irrational number is two.