English
Let f: F →* K and p ∈ F[X] be monic with p.natDegree ≤ d, and all roots of map f p have modulus ≤ B. Then for each coefficient i, ∥(map f p).coeff i∥ ≤ max{B,1}^d · d choose floor(d/2).
Русский
Пусть f: F →* K и p ∈ F[X] моноичен, deg(p) ≤ d, и все корни map f p имеют модуль ≤ B. Тогда для любого коэффициента i выполняется ∥coeff i∥ ≤ max{B,1}^d · dC floor(d/2).
LaTeX
$$$p\\text{ моноичен},\\; p. natDegree ≤ d,\\; (\\forall z ∈ (map f p).roots, \\|z\\| ≤ B) \\Rightarrow ∥(map f p).coeff i∥ ≤ \\max(B,1)^d \\binom{d}{\\lfloor d/2\\rfloor}$$$
Lean4
/-- The coefficients of the monic polynomials of bounded degree with bounded roots are
uniformly bounded. -/
theorem coeff_bdd_of_roots_le {B : ℝ} {d : ℕ} (f : F →+* K) {p : F[X]} (h1 : p.Monic) (h2 : Splits f p)
(h3 : p.natDegree ≤ d) (h4 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) (i : ℕ) :
‖(map f p).coeff i‖ ≤ max B 1 ^ d * d.choose (d / 2) :=
by
obtain hB | hB := le_or_gt 0 B
· apply (coeff_le_of_roots_le i h1 h2 h4).trans
calc
_ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left
_ ≤ max B 1 ^ d * p.natDegree.choose i := by
gcongr
· apply le_max_right
· exact le_trans (Nat.sub_le _ _) h3
_ ≤ max B 1 ^ d * d.choose (d / 2) := by gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d)
· rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]
refine le_trans ?_ (one_le_mul_of_one_le_of_one_le (one_le_pow₀ (le_max_right B 1)) ?_)
· split_ifs <;> norm_num
· exact mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))
