The binary form of a complex polynomial near one of its roots

Let f ∈ ℂ[X] have degree d and let F(x, y) = y ^ d f(x / y) be its homogenization of degree d. If α is a root of f, then F is small at points (x, y) close to the line x = α y: writing f = a ∏ (X - αᵢ) with α₁ = α, every other factor of F(x, y) = a ∏ (x - αᵢ y) is at most 2 max(1, |αᵢ|) max(|x|, |y|), which gives |F(x, y)| ≤ 2 ^ (d - 1) M(f) max(|x|, |y|) ^ (d - 1) |x - α y|, where M(f) is the Mahler measure. Dividing by y turns this into a bound by the distance |x / y - α|.

Applied to a polynomial with integer coefficients at an integer point where F does not vanish, the left-hand side is at least 1; this is Liouville's inequality.

Main results

• Polynomial.norm_eval_homogenize_le_mahlerMeasure_mul: ‖F(x)‖ ≤ 2 ^ (d - 1) M(f) ‖x‖ ^ (d - 1) ‖x 0 - α x 1‖ for every x : Fin 2 → ℂ.
• Polynomial.norm_eval_homogenize_le_mahlerMeasure_mul_norm_div_sub: ‖F(x)‖ ≤ 2 ^ (d - 1) M(f) ‖x‖ ^ d ‖x 0 / x 1 - α‖ when x 1 ≠ 0.

Here ‖x‖ = max ‖x 0‖ ‖x 1‖ is the sup norm on Fin 2 → ℂ.

References

• J.-H. Evertse, Diophantine Approximation, lecture notes (2019), ch. 6, proof of Theorem 6.1.

theorem Polynomial.norm_eval_homogenize_le_mahlerMeasure_mul (f : Polynomial ℂ) {α : ℂ} (hα : f.IsRoot α) (x : Fin 2 → ℂ) : ‖(MvPolynomial.eval x) (f.homogenize f.natDegree)‖ ≤ 2 ^ (f.natDegree - 1) * f.mahlerMeasure * ‖x‖ ^ (f.natDegree - 1) * ‖x 0 - α * x 1‖

If α is a root of f ∈ ℂ[X] of degree d, the homogenization F of f in degree d satisfies ‖F(x)‖ ≤ 2 ^ (d - 1) M(f) ‖x‖ ^ (d - 1) ‖x 0 - α x 1‖ at every point x : Fin 2 → ℂ, where M(f) is the Mahler measure and ‖x‖ the sup norm.

theorem Polynomial.norm_eval_homogenize_le_mahlerMeasure_mul_norm_div_sub (f : Polynomial ℂ) {α : ℂ} (hα : f.IsRoot α) {x : Fin 2 → ℂ} (hx : x 1 ≠ 0) : ‖(MvPolynomial.eval x) (f.homogenize f.natDegree)‖ ≤ 2 ^ (f.natDegree - 1) * f.mahlerMeasure * ‖x‖ ^ f.natDegree * ‖x 0 / x 1 - α‖

If α is a root of f ∈ ℂ[X] of degree d, the homogenization F of f in degree d satisfies ‖F(x)‖ ≤ 2 ^ (d - 1) M(f) ‖x‖ ^ d ‖x 0 / x 1 - α‖ at every point x : Fin 2 → ℂ with x 1 ≠ 0, where M(f) is the Mahler measure and ‖x‖ the sup norm.