Nonvanishing derivatives of Thue's auxiliary polynomials

Let α be algebraic of degree d ≥ 2 over a field K of characteristic zero, and let P, Q ∈ K[X], not both zero, of degree at most N < d r, be such that (X - α) ^ r divides P - α Q. Thue's auxiliary polynomials (TauCeti.exists_thue_auxiliary_polynomials) are of this form. For every pair of points ξ₁, ξ₂ ∈ K there is then a Hasse derivative order k ≤ 2 N - d (r - 1) with Dᵏ P (ξ₁) ≠ ξ₂ Dᵏ Q (ξ₁). For Thue's polynomials, where N = ⌊(1 / 2 + ε) d r⌋, this order is at most d (2 ε r + 1).

In Thue's proof, ξ₁ and ξ₂ are two good rational approximations of α. The nonzero rational number Dᵏ P (ξ₁) - ξ₂ Dᵏ Q (ξ₁) has bounded denominator, hence is not too small, whereas it is small because ξ₁ and ξ₂ are close to α; the order k is small enough for the two estimates to clash.

The proof considers the Wronskian W = Q P' - Q' P. It is nonzero, because P and Q are linearly independent (a dependence would make minpoly K α ^ r divide P or Q, contradicting N < d r). Since W is also the Wronskian of Q and P - α Q, it is divisible by (X - α) ^ (r - 1) and hence, by minpoly.pow_dvd_iff, by minpoly K α ^ (r - 1). Similarly, if ξ₁ is a root of multiplicity m of P - ξ₂ Q, then (X - ξ₁) ^ (m - 1) divides W. Since W has degree less than 2 N, comparing degrees gives m + d (r - 1) ≤ 2 N, and the Hasse derivative of P - ξ₂ Q of order m does not vanish at ξ₁.

Main results

• TauCeti.exists_hasseDeriv_eval_ne_mul_of_dvd: the general statement over a field K of characteristic zero, with k + d (r - 1) ≤ 2 N.
• TauCeti.exists_hasseDeriv_aeval_ne_mul_of_natDegree_le: the integer-polynomial form, retaining the natural-degree bound and k ≤ N.
• TauCeti.exists_hasseDeriv_aeval_ne_mul_of_dvd: the form used in Thue's theorem, for integer polynomials of degree at most ⌊(1 / 2 + ε) d r⌋, rational points ξ₁, ξ₂ and k ≤ d (2 ε r + 1).

References

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

theorem TauCeti.exists_hasseDeriv_eval_ne_mul_of_dvd {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [CharZero K] {α : L} (hd : 2 ≤ (minpoly K α).natDegree) {P Q : Polynomial K} (hPQ : P ≠ 0 ∨ Q ≠ 0) {N r : ℕ} (hP : P.natDegree ≤ N) (hQ : Q.natDegree ≤ N) (hN : N < (minpoly K α).natDegree * r) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (algebraMap K L) P - Polynomial.C α * Polynomial.map (algebraMap K L) Q) (ξ₁ ξ₂ : K) : ∃ (k : ℕ), k + (minpoly K α).natDegree * (r - 1) ≤ 2 * N ∧ Polynomial.eval ξ₁ ((Polynomial.hasseDeriv k) P) ≠ ξ₂ * Polynomial.eval ξ₁ ((Polynomial.hasseDeriv k) Q)

Nonvanishing derivatives of Thue's polynomials. Let α be algebraic of degree d ≥ 2 over a field K of characteristic zero, and let P, Q ∈ K[X], not both zero, of degree at most N < d r, be such that (X - α) ^ r divides P - α Q. For all ξ₁, ξ₂ ∈ K there is a k with k + d (r - 1) ≤ 2 N such that the k-th Hasse derivatives satisfy Dᵏ P (ξ₁) ≠ ξ₂ Dᵏ Q (ξ₁).

theorem TauCeti.exists_hasseDeriv_aeval_ne_mul_of_natDegree_le {F : Type u_3} [Field F] [CharZero F] {α : F} (hd : 2 ≤ (minpoly ℚ α).natDegree) {P Q : Polynomial ℤ} (hPQ : P ≠ 0 ∨ Q ≠ 0) {N r : ℕ} (hP : P.natDegree ≤ N) (hQ : Q.natDegree ≤ N) (hN : N < (minpoly ℚ α).natDegree * r) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (Int.castRingHom F) P - Polynomial.C α * Polynomial.map (Int.castRingHom F) Q) (ξ₁ ξ₂ : ℚ) : ∃ k ≤ N, k + (minpoly ℚ α).natDegree * (r - 1) ≤ 2 * N ∧ (Polynomial.aeval ξ₁) ((Polynomial.hasseDeriv k) P) ≠ ξ₂ * (Polynomial.aeval ξ₁) ((Polynomial.hasseDeriv k) Q)

The integer-polynomial form of derivative nonvanishing, retaining the natural-degree bound k + d (r - 1) ≤ 2 N. The nonzero derivative also forces k ≤ N.

theorem TauCeti.thue_order_le_of_add_mul_le {d r k N : ℕ} {ε : ℝ} (hr : 0 < r) (hN : ↑N ≤ (1 / 2 + ε) * ↑d * ↑r) (hk : k + d * (r - 1) ≤ 2 * N) : ↑k ≤ ↑d * (2 * ε * ↑r + 1)

Convert the natural-degree order bound into the real order bound used in Thue's construction, whenever the auxiliary degree is at most (1 / 2 + ε) d r.

theorem TauCeti.exists_hasseDeriv_aeval_ne_mul_of_dvd {F : Type u_3} [Field F] [CharZero F] {α : F} (hd : 2 ≤ (minpoly ℚ α).natDegree) {ε : ℝ} (hε₀ : 0 ≤ ε) (hε : ε < 1 / 2) {r : ℕ} (hr : 0 < r) {P Q : Polynomial ℤ} (hPQ : P ≠ 0 ∨ Q ≠ 0) (hP : P.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊) (hQ : Q.natDegree ≤ ⌊(1 / 2 + ε) * ↑(minpoly ℚ α).natDegree * ↑r⌋₊) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ Polynomial.map (Int.castRingHom F) P - Polynomial.C α * Polynomial.map (Int.castRingHom F) Q) (ξ₁ ξ₂ : ℚ) : ∃ (k : ℕ), ↑k ≤ ↑(minpoly ℚ α).natDegree * (2 * ε * ↑r + 1) ∧ (Polynomial.aeval ξ₁) ((Polynomial.hasseDeriv k) P) ≠ ξ₂ * (Polynomial.aeval ξ₁) ((Polynomial.hasseDeriv k) Q)

Nonvanishing derivatives of Thue's polynomials, in the form used in Thue's theorem. Let α be algebraic of degree d ≥ 2 over ℚ, let 0 ≤ ε < 1 / 2 and r ≥ 1, and let P, Q be integer polynomials, not both zero, of degree at most ⌊(1 / 2 + ε) d r⌋, such that (X - α) ^ r divides P - α Q. For all rational numbers ξ₁, ξ₂ there is a k ≤ d (2 ε r + 1) such that the k-th Hasse derivatives satisfy Dᵏ P (ξ₁) ≠ ξ₂ Dᵏ Q (ξ₁).