Thue's auxiliary polynomials

Let α be an algebraic number of degree d, let b ≥ 1 be an integer with b α integral, and let 0 < ε < 1 / 2. For every r ≥ 1 there are integer polynomials P and Q, not both zero, of degree at most ⌊(1 / 2 + ε) d r⌋ such that (X - α) ^ r divides P - α Q, and whose coefficient lengths are at most C₁ ^ r, where C₁ = (48 b max(1, ⌈α⌉)) ^ (d (1 + 1 / ε)) and ⌈α⌉ is the house of α.

These polynomials are the auxiliary construction in Thue's proof that an algebraic number of degree d ≥ 3 has only finitely many rational approximations ξ with |ξ - α| ≤ H(ξ) ^ (-κ) for κ > d / 2 + 1: the polynomial P - α Q vanishes to high order at α, so it is small near α, while its coefficients stay small because of the length bound.

The vanishing conditions are r linear equations over the number field ℚ(α) for the 2 (m + 1) integer coefficients of P and Q, where m = ⌊(1 / 2 + ε) d r⌋. Since d r < 2 (m + 1), Siegel's lemma (NumberField.exists_ne_zero_int_vec_abs_le_of_house_le) gives a small nonzero integer solution.

Main results

• TauCeti.exists_thue_auxiliary_polynomials: Thue's auxiliary polynomials, for an element α of any field of characteristic zero.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, Lemma 6.10.

theorem TauCeti.exists_thue_auxiliary_polynomials {F : Type u_2} [Field F] [CharZero F] {α : F} {b : ℕ} (hb : 0 < b) (hbα : IsIntegral ℤ (↑b * α)) {ε : ℝ} (hε₀ : 0 < ε) (hε : ε < 1 / 2) {r : ℕ} (hr : 0 < r) : ∃ (P : Polynomial ℤ) (Q : Polynomial ℤ), (P ≠ 0 ∨ Q ≠ 0) ∧ P.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊ ∧ Q.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊ ∧ (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (Int.castRingHom F) P - Polynomial.C α * Polynomial.map (Int.castRingHom F) Q ∧ P.l1Norm ≤ ((48 * ↑b * max 1 (house α)) ^ (↑(minpoly ℚ α).natDegree * (1 + 1 / ε))) ^ r ∧ Q.l1Norm ≤ ((48 * ↑b * max 1 (house α)) ^ (↑(minpoly ℚ α).natDegree * (1 + 1 / ε))) ^ r

Thue's auxiliary polynomials (Evertse, Lemma 6.10). Let α be an algebraic number of degree d in a field of characteristic zero, and let b ≥ 1 be an integer such that b α is integral over ℤ. For 0 < ε < 1 / 2 and r ≥ 1 there are integer polynomials P and Q, not both zero, of degree at most ⌊(1 / 2 + ε) d r⌋, such that (X - α) ^ r divides P - α Q and both coefficient lengths are at most C₁ ^ r, where C₁ = (48 b max(1, ⌈α⌉)) ^ (d (1 + 1 / ε)) and ⌈α⌉ is the house of α.