Values of Thue's auxiliary polynomials near α

Let P and Q be polynomials of degree at most δ r with coefficient lengths at most C₁ ^ r, where r > 0, and suppose that Dᵏ P - α Dᵏ Q = V (X - α) ^ m for a Hasse derivative Dᵏ and some m. Then on the closed unit ball around α both V and Dᵏ Q are bounded by C₂ ^ r, where C₂ = 2 ^ δ (1 + ‖α‖) ^ (1 + δ) C₁.

For Thue's auxiliary polynomials (TauCeti.exists_thue_auxiliary_polynomials), mapped from ℤ[X] to ℂ[X] (which preserves coefficient length by Polynomial.l1Norm_map), one takes δ = (1 / 2 + ε) d, where d is the degree of α, and m = r - k. In Thue's gap principle the bound is applied at a good rational approximation ξ₁ of α: there Dᵏ P (ξ₁) - ξ₂ Dᵏ Q (ξ₁) = V (ξ₁) (ξ₁ - α) ^ (r - k) + (α - ξ₂) Dᵏ Q (ξ₁). The factors V (ξ₁) and Dᵏ Q (ξ₁) are at most C₂ ^ r, while ξ₁ - α and α - ξ₂ are small.

If (X - α) ^ r divides P - α Q, the two bounds combine to ‖Dᵏ P (z) - w Dᵏ Q (z)‖ ≤ C₂ ^ r (‖z - α‖ ^ (r - k) + ‖w - α‖) for ‖z - α‖ ≤ 1 and every w.

The derivative bound holds over any seminormed ring, and the quotient bound over any seminormed commutative ring, as in the motivating example ℂ.

Main results

• TauCeti.norm_eval_hasseDeriv_le_pow_of_norm_sub_le_one: the bound for Dᵏ Q.
• TauCeti.norm_eval_le_pow_of_hasseDeriv_sub_eq_mul: the bound for V.
• TauCeti.norm_eval_hasseDeriv_sub_mul_le: the bound for Dᵏ P (z) - w Dᵏ Q (z).

References

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

theorem TauCeti.norm_eval_hasseDeriv_le_pow_of_norm_sub_le_one {R : Type u_1} [SeminormedRing R] {Q : Polynomial R} {α z : R} {k r : ℕ} {δ C₁ : ℝ} (hQ : ↑Q.natDegree ≤ δ * ↑r) (hQC : Q.l1Norm ≤ C₁ ^ r) (hz : ‖z - α‖ ≤ 1) : ‖Polynomial.eval z ((Polynomial.hasseDeriv k) Q)‖ ≤ (2 ^ δ * (1 + ‖α‖) ^ (1 + δ) * C₁) ^ r

Values of Hasse derivatives near α (Evertse, Lemma 6.13). Let Q have degree at most δ r and coefficient length at most C₁ ^ r. Then every Hasse derivative Dᵏ Q is bounded by C₂ ^ r on the closed unit ball around α, where C₂ = 2 ^ δ (1 + ‖α‖) ^ (1 + δ) C₁.

theorem TauCeti.norm_eval_le_pow_of_hasseDeriv_sub_eq_mul {R : Type u_1} [SeminormedCommRing R] {P Q V : Polynomial R} {α z : R} {k m r : ℕ} {δ C₁ : ℝ} (hr : 0 < r) (hP : ↑P.natDegree ≤ δ * ↑r) (hQ : ↑Q.natDegree ≤ δ * ↑r) (hPC : P.l1Norm ≤ C₁ ^ r) (hQC : Q.l1Norm ≤ C₁ ^ r) (hV : (Polynomial.hasseDeriv k) P - Polynomial.C α * (Polynomial.hasseDeriv k) Q = V * (Polynomial.X - Polynomial.C α) ^ m) (hz : ‖z - α‖ ≤ 1) : ‖Polynomial.eval z V‖ ≤ (2 ^ δ * (1 + ‖α‖) ^ (1 + δ) * C₁) ^ r

Values of Thue's quotient polynomial near α (Evertse, Lemma 6.13). Let r > 0, let P and Q have degree at most δ r and coefficient length at most C₁ ^ r, and suppose that Dᵏ P - α Dᵏ Q = V (X - α) ^ m. Then V is bounded by C₂ ^ r on the closed unit ball around α, where C₂ = 2 ^ δ (1 + ‖α‖) ^ (1 + δ) C₁.

theorem TauCeti.norm_eval_hasseDeriv_sub_mul_le {R : Type u_1} [SeminormedCommRing R] {P Q : Polynomial R} {α z : R} (w : R) (k : ℕ) {r : ℕ} {δ C₁ : ℝ} (hr : 0 < r) (hP : ↑P.natDegree ≤ δ * ↑r) (hQ : ↑Q.natDegree ≤ δ * ↑r) (hPC : P.l1Norm ≤ C₁ ^ r) (hQC : Q.l1Norm ≤ C₁ ^ r) (hdvd : (Polynomial.X - Polynomial.C α) ^ r ∣ P - Polynomial.C α * Q) (hz : ‖z - α‖ ≤ 1) : ‖Polynomial.eval z ((Polynomial.hasseDeriv k) P) - w * Polynomial.eval z ((Polynomial.hasseDeriv k) Q)‖ ≤ (2 ^ δ * (1 + ‖α‖) ^ (1 + δ) * C₁) ^ r * (‖z - α‖ ^ (r - k) + ‖w - α‖)

Values of Thue's auxiliary polynomials at two points near α (Evertse, proof of Theorem 6.14). Let r > 0, let P and Q have degree at most δ r and coefficient length at most C₁ ^ r, and suppose that (X - α) ^ r divides P - α Q. If ‖z - α‖ ≤ 1, then for every k and w, ‖Dᵏ P (z) - w Dᵏ Q (z)‖ ≤ C₂ ^ r (‖z - α‖ ^ (r - k) + ‖w - α‖), where C₂ = 2 ^ δ (1 + ‖α‖) ^ (1 + δ) C₁.