Root bounds in terms of the coefficient sup norm

Reversing the coefficients preserves the sup norm. Cauchy's root bound, together with the fact that a nonzero integer has modulus at least one, bounds every real or complex root of an integer polynomial by its sup norm plus one. Applying this to the reversed polynomial also bounds nonzero roots away from zero.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 3, Exercise 3.1(ii).

The root estimate uses Mathlib's Polynomial.IsRoot.norm_lt_cauchyBound.

theorem Polynomial.norm_lt_supNorm_add_one_of_aeval_eq_zero {K : Type u_1} [RCLike K] (p : Polynomial ℤ) (hp : p ≠ 0) {z : K} (hz : (aeval z) p = 0) : ‖z‖ < p.supNorm + 1

A real or complex root of a nonzero integer polynomial has modulus strictly less than its coefficient sup norm plus one.

theorem Polynomial.inv_supNorm_add_one_lt_norm_of_aeval_eq_zero {K : Type u_1} [RCLike K] (p : Polynomial ℤ) (hp : p ≠ 0) {z : K} (hz : (aeval z) p = 0) (hz0 : z ≠ 0) : (p.supNorm + 1)⁻¹ < ‖z‖

A nonzero real or complex root of a nonzero integer polynomial has modulus strictly greater than the reciprocal of its coefficient sup norm plus one.