Roth's theorem for binary forms

Let F ∈ ℤ[X₀, X₁] be a binary form of degree d with no squared linear factor over ℂ. Roth's theorem gives the Thue–Roth inequality: for every κ > 2 there is c > 0 with

|F(x, y)| ≥ c max(|x|, |y|) ^ (d - κ) whenever x, y ∈ ℤ and F(x, y) ≠ 0.

Over ℂ, F = a ∏ᵢ Lᵢ is a product of d pairwise non-proportional linear forms, each X₁ or X₀ - α X₁ with α algebraic (MvPolynomial.IsHomogeneous.exists_linear_factors). At an integer point (x, y) with M = max(|x|, |y|):

• by Cramer's rule, two non-proportional forms cannot both be much smaller than M (TauCeti.norm_det_mul_max_norm_le), so all forms but the smallest one are at least c M (TauCeti.exists_pos_mul_max_norm_le_norm_of_pairwise);
• by Roth's theorem for α, the smallest one is still at least c M ^ (1 - κ) (IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul).

Multiplying gives |F(x, y)| ≥ c M ^ (d - 1) M ^ (1 - κ) (TauCeti.exists_pos_mul_max_abs_rpow_le_prod_norm). Like Roth's theorem, the inequality is ineffective. For d ≥ 3 it is the analytic input to Thue's theorem on the equations F(x, y) = m with m ≠ 0: choosing 2 < κ < d bounds max(|x|, |y|) on the solutions of 0 < |F(x, y)| ≤ B. An arbitrary binary form F such that F(X, 1) has at least three distinct complex zeros has such a divisor G ∣ F of degree at least 3 (MvPolynomial.IsHomogeneous.exists_dvd_isHomogeneous_not_sq_dvd), and G(x, y) divides F(x, y), so Thue's theorem holds for F as well.

Main results

• IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul: Roth's theorem for the linear form x - α y: ‖x - α y‖ ≥ c max(|x|, |y|) ^ (1 - κ) for integers with x ≠ α y.
• TauCeti.exists_pos_mul_max_abs_rpow_le_prod_norm: a product of pairwise non-proportional linear forms satisfying such bounds is at least c max(|x|, |y|) ^ (#T - κ).
• MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval: the Thue–Roth inequality for binary forms without squared linear factors.
• MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le, MvPolynomial.IsHomogeneous.finite_setOf_eval_eq: the Thue inequality 0 < |F(x, y)| ≤ B and Thue's equation F(x, y) = m with m ≠ 0 have finitely many integer solutions, for such forms of degree d ≥ 3.
• MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots, MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots: the same for binary forms F such that F(X, 1) has at least three distinct complex zeros (Thue's theorem).
• TauCeti.finite_setOf_mul_pow_add_mul_pow_eq: the binomial Thue equation a x ^ n + c y ^ n = m with n ≥ 3 and a, c, m ≠ 0 has finitely many integer solutions.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Theorem 6.3 and Corollary 6.4.
• A. Thue, Über Annäherungswerte algebraischer Zahlen, J. Reine Angew. Math. 135 (1909), 284–305.

theorem IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul {α : ℂ} (hα : IsAlgebraic ℚ α) {κ : ℝ} (hκ : 2 < κ) : ∃ (c : ℝ), 0 < c ∧ ∀ (x y : ℤ), ↑x - α * ↑y ≠ 0 → c * max |↑x| |↑y| ^ (1 - κ) ≤ ‖↑x - α * ↑y‖

Roth's theorem for a linear form. If α ∈ ℂ is algebraic and κ > 2, then there is c > 0 with ‖x - α y‖ ≥ c max(|x|, |y|) ^ (1 - κ) for all integers x, y with x ≠ α y.

theorem TauCeti.exists_pos_mul_max_abs_rpow_le_prod_norm {T : Finset (ℂ × ℂ)} (hT : (↑T).Pairwise fun (ℓ ℓ' : ℂ × ℂ) => ℓ.1 * ℓ'.2 - ℓ.2 * ℓ'.1 ≠ 0) {κ : ℝ} (hκ : 0 ≤ κ) (hL : ∀ ℓ ∈ T, ∃ (c : ℝ), 0 < c ∧ ∀ (x y : ℤ), ℓ.1 * ↑x + ℓ.2 * ↑y ≠ 0 → c * max |↑x| |↑y| ^ (1 - κ) ≤ ‖ℓ.1 * ↑x + ℓ.2 * ↑y‖) : ∃ (c : ℝ), 0 < c ∧ ∀ (x y : ℤ), (∀ ℓ ∈ T, ℓ.1 * ↑x + ℓ.2 * ↑y ≠ 0) → c * max |↑x| |↑y| ^ (↑T.card - κ) ≤ ∏ ℓ ∈ T, ‖ℓ.1 * ↑x + ℓ.2 * ↑y‖

Let ℓ.1 x + ℓ.2 y, ℓ ∈ T, be pairwise non-proportional complex linear forms, each bounded below by c max(|x|, |y|) ^ (1 - κ) at the integer points where it does not vanish, for some κ ≥ 0. Then there is c > 0 with ∏_{ℓ ∈ T} ‖ℓ.1 x + ℓ.2 y‖ ≥ c max(|x|, |y|) ^ (#T - κ) at every integer point where no form vanishes.

theorem MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (hsq : ∀ (a b : ℂ), (a, b) ≠ (0, 0) → ¬(C a * X 0 + C b * X 1) ^ 2 ∣ (map (Int.castRingHom ℂ)) F) {κ : ℝ} (hκ : 2 < κ) : ∃ (c : ℝ), 0 < c ∧ ∀ (x y : ℤ), (eval ![x, y]) F ≠ 0 → c * max |↑x| |↑y| ^ (↑d - κ) ≤ |↑((eval ![x, y]) F)|

The Thue–Roth inequality for binary forms (Evertse, Theorem 6.3). Let F ∈ ℤ[X₀, X₁] be a binary form of degree d with no squared linear factor over ℂ, and let κ > 2. Then there is c > 0 with |F(x, y)| ≥ c max(|x|, |y|) ^ (d - κ) for all integers x, y with F(x, y) ≠ 0. The proof is ineffective: it gives no value of c.

theorem MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (hsq : ∀ (a b : ℂ), (a, b) ≠ (0, 0) → ¬(C a * X 0 + C b * X 1) ^ 2 ∣ (map (Int.castRingHom ℂ)) F) (hd : 3 ≤ d) (B : ℤ) : {p : ℤ × ℤ | (eval ![p.1, p.2]) F ≠ 0 ∧ |(eval ![p.1, p.2]) F| ≤ B}.Finite

The Thue inequality for square-free binary forms (Evertse, Corollary 6.4, square-free case). Let F ∈ ℤ[X₀, X₁] be a binary form of degree d ≥ 3 with no squared linear factor over ℂ. Then for every bound B, the inequality 0 < |F(x, y)| ≤ B has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

theorem MvPolynomial.IsHomogeneous.finite_setOf_eval_eq {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (hsq : ∀ (a b : ℂ), (a, b) ≠ (0, 0) → ¬(C a * X 0 + C b * X 1) ^ 2 ∣ (map (Int.castRingHom ℂ)) F) (hd : 3 ≤ d) {m : ℤ} (hm : m ≠ 0) : {p : ℤ × ℤ | (eval ![p.1, p.2]) F = m}.Finite

Thue's theorem for square-free binary forms (Evertse, Corollary 6.4, square-free case). Let F ∈ ℤ[X₀, X₁] be a binary form of degree d ≥ 3 with no squared linear factor over ℂ, and let m ≠ 0. Then the Thue equation F(x, y) = m has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

theorem MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (hroots : 3 ≤ (Polynomial.map (Int.castRingHom ℂ) ((MvPolynomial.aeval ![Polynomial.X, 1]) F)).roots.toFinset.card) (B : ℤ) : {p : ℤ × ℤ | (eval ![p.1, p.2]) F ≠ 0 ∧ |(eval ![p.1, p.2]) F| ≤ B}.Finite

The Thue inequality (Evertse, Corollary 6.4). Let F ∈ ℤ[X₀, X₁] be a binary form such that F(X, 1) has at least three distinct complex zeros. Then for every bound B, the inequality 0 < |F(x, y)| ≤ B has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

theorem MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d) (hroots : 3 ≤ (Polynomial.map (Int.castRingHom ℂ) ((MvPolynomial.aeval ![Polynomial.X, 1]) F)).roots.toFinset.card) {m : ℤ} (hm : m ≠ 0) : {p : ℤ × ℤ | (eval ![p.1, p.2]) F = m}.Finite

Thue's theorem (Thue 1909; Evertse, Corollary 6.4). Let F ∈ ℤ[X₀, X₁] be a binary form such that F(X, 1) has at least three distinct complex zeros, and let m ≠ 0. Then the Thue equation F(x, y) = m has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

theorem TauCeti.finite_setOf_mul_pow_add_mul_pow_eq {n : ℕ} (hn : 3 ≤ n) {a c m : ℤ} (ha : a ≠ 0) (hc : c ≠ 0) (hm : m ≠ 0) : {p : ℤ × ℤ | a * p.1 ^ n + c * p.2 ^ n = m}.Finite

Binomial Thue equations. For n ≥ 3 and nonzero integers a, c and m, the equation a x ^ n + c y ^ n = m has only finitely many integer solutions: a X ^ n + c has n distinct complex zeros. Like Thue's theorem, the proof is ineffective.