Northcott's theorem for integer polynomials and the height gaps

The coefficient sup norm Polynomial.supNorm of an integer polynomial is its naive height. Over ℤ only finitely many polynomials have bounded degree and bounded naive height (Polynomial.finite_setOf_natDegree_le_supNorm_le). This fails over ℚ, where the constants 1 / k all have height at most 1, and it fails without the degree bound, where the powers of X all have height 1.

Two consequences make Northcott's theorem usable in Diophantine approximation by algebraic numbers, where solutions are integer polynomials P with ‖P ξ‖ small, or roots α with ‖ξ - α‖ small, compared to a negative power of the height. Fix a degree bound n and a height bound B. Then

• there is δ > 0 such that every integer polynomial P of degree at most n with 0 < ‖P ξ‖ < δ has naive height above B (Polynomial.exists_pos_lt_supNorm_of_norm_aeval_lt);
• there is δ > 0 such that every nonzero integer polynomial Q of degree at most n with a root α ≠ ξ satisfying ‖ξ - α‖ < δ has naive height above B (Polynomial.exists_pos_lt_supNorm_of_norm_sub_root_lt).

In both cases the finitely many polynomials of degree at most n and height at most B give only finitely many nonzero values at ξ, respectively finitely many roots other than ξ, and δ is chosen below all of their sizes. These height gaps are what lets an exponent defined by infinitely many solutions of bounded degree be controlled through their heights.

The value gap holds for ξ in an arbitrary normed ring, and the root gap for ξ in a normed commutative domain of characteristic zero, so the statements apply both to real approximation by real algebraic numbers and to real or complex approximation by complex algebraic numbers.

References

• Y. Bugeaud, Approximation by Algebraic Numbers, Cambridge University Press (2004), §3.1.
• E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), §1.6.

The statements are adapted from Ralf Stephan's DiophantineApproximation/PolynomialSupNorm.lean in rwst/Subspace-Theorems, commit 09835cb23557ae5ae0cf55a9c4ab9055f5d60338 (Apache 2.0). Here they are restated at the normed-ring level, and the proofs reuse the bounded-coefficient finiteness of integer polynomials.

theorem Polynomial.finite_setOf_natDegree_le_supNorm_le (n : ℕ) (B : ℝ) : {P : Polynomial ℤ | P.natDegree ≤ n ∧ P.supNorm ≤ B}.Finite

Northcott's theorem for integer polynomials. Only finitely many integer polynomials have degree at most n and coefficient sup norm (naive height) at most B.

theorem Polynomial.exists_pos_lt_supNorm_of_norm_aeval_lt {A : Type u_1} [NormedRing A] (ξ : A) (n : ℕ) (B : ℝ) : ∃ δ > 0, ∀ (P : Polynomial ℤ), P.natDegree ≤ n → (aeval ξ) P ≠ 0 → ‖(aeval ξ) P‖ < δ → B < P.supNorm

The height gap for values. For a degree bound n and a height bound B there is δ > 0 such that every integer polynomial P of degree at most n with aeval ξ P ≠ 0 and ‖aeval ξ P‖ < δ has coefficient sup norm greater than B.

theorem Polynomial.exists_pos_lt_supNorm_of_norm_sub_root_lt {A : Type u_1} [NormedCommRing A] [IsDomain A] [CharZero A] (ξ : A) (n : ℕ) (B : ℝ) : ∃ δ > 0, ∀ (Q : Polynomial ℤ) (α : A), Q.natDegree ≤ n → Q ≠ 0 → (aeval α) Q = 0 → α ≠ ξ → ‖ξ - α‖ < δ → B < Q.supNorm

The height gap for roots. For a degree bound n and a height bound B there is δ > 0 such that every nonzero integer polynomial Q of degree at most n with a root α ≠ ξ satisfying ‖ξ - α‖ < δ has coefficient sup norm greater than B.