The Gelfond bound for polynomial factors

For complex polynomials with product of degree d, the product of the coefficient sup norms is at most 2 ^ d times the sup norm of the product. Together with the reverse bound in SupNorm.Basic, this controls coefficient heights under factorization. Zero factors and empty products are included.

The Gelfond bound combines Mathlib's coefficient-to-Mahler and Landau estimates with supermultiplicativity and the square-root bound for middle binomial coefficients.

References

• Xiaorun Wu, Diophantine geometry, week 08: arithmetic heights (2023), Lemmas 3.5–3.6.
• Lukas Pottmeyer, Diophantine Approximation (2022), Lemma 3.2.10.

theorem Polynomial.prod_supNorm_le_two_pow_mul_supNorm_prod {ι : Type u_1} (s : Finset ι) (f : ι → Polynomial ℂ) : ∏ i ∈ s, (f i).supNorm ≤ 2 ^ (∏ i ∈ s, f i).natDegree * (∏ i ∈ s, f i).supNorm

The Gelfond factor bound: the product of the coefficient sup norms of complex polynomials is at most 2^d times the sup norm of their degree-d product.