Coefficient bounds in terms of root bounds

Mathlib's Polynomial.coeff_le_of_roots_le bounds every coefficient of a monic polynomial by B ^ (p.natDegree - i) times a binomial coefficient, where B bounds all its roots. This file adds the estimate for the constant coefficient that keeps the factor of a distinguished root w separate:

‖p.coeff 0‖ ≤ ‖w‖ * B ^ (p.natDegree - 1)

for a monic p with a root w and all roots in the closed disc of radius B.

Main results

• Polynomial.norm_coeff_zero_le_norm_mul_pow_of_roots_le: the constant coefficient of a monic polynomial with bounded roots is at most ‖w‖ * B ^ (p.natDegree - 1) at each root w.

theorem Polynomial.norm_coeff_zero_le_norm_mul_pow_of_roots_le {K : Type u_1} [NormedField K] {p : Polynomial K} {B : ℝ} (hp : p.Monic) (hs : p.Splits) (hB : ∀ z ∈ p.roots, ‖z‖ ≤ B) {w : K} (hw : p.IsRoot w) : ‖p.coeff 0‖ ≤ ‖w‖ * B ^ (p.natDegree - 1)

The constant coefficient against a distinguished root. A monic polynomial p that splits over a normed field, all of whose roots are bounded by B, has constant coefficient at most ‖w‖ * B ^ (p.natDegree - 1) at each root w: it is ±w times the product of the remaining roots, each of modulus at most B.

theorem Polynomial.norm_coeff_le_of_roots_erase_le {K : Type u_1} [NormedField K] [DecidableEq K] {p : Polynomial K} {B : ℝ} (hp : p.Monic) (hs : p.Splits) {w : K} (hw : p.IsRoot w) (hwB : ‖w‖ ≤ B) (hB : ∀ z ∈ p.roots.erase w, ‖z‖ ≤ 1) {k : ℕ} (hk : 0 < k) (hkn : k < p.natDegree) : ‖p.coeff (p.natDegree - k)‖ ≤ ↑((p.natDegree - 1).choose (k - 1)) * B + ↑((p.natDegree - 1).choose k)

The coefficients against a distinguished root. A monic polynomial p that splits over a normed field, with a root w of norm at most B whose remaining roots have norm at most 1, has its coefficient of X ^ (n - k), for 0 < k < n = p.natDegree, bounded in norm by C(n-1, k-1) * B + C(n-1, k): it is q_(n-k-1) - w * q_(n-k) for the cofactor q of X - w, whose coefficients are bounded by Mathlib's coeff_le_of_roots_le.