English
Let f: F →* K and p ∈ F[X] be monic and split. If B bounds the roots of map f p and i any index, then the i-th coefficient of map f p is bounded by a function of B and deg p, namely ∥(map f p).coeff i∥ ≤ max(B,1)^{deg p} · deg p choose i.
Русский
Пусть f: F →* K и p ∈ F[X] моноичен и раскладывается. Если B ограничивает корни map f p, и i любая, то i-й коэффициент map f p ограничен функцией от B и степени p: ∥coeff i∥ ≤ max(B,1)^{deg p} · deg p выбор i.
LaTeX
$$$\\text{p Mo n ic} \\land \\text{Splits } f p \\land\\; (\\forall z \\in (map f p).roots, \\|z\\| \\le B) \\Rightarrow \\| (map f p).coeff i \\| \\le \\max(B,1)^{p. natDegree} \\binom{p. natDegree}{i}$$$
Lean4
theorem coeff_le_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.Monic) (h2 : Splits f p)
(h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) : ‖(map f p).coeff i‖ ≤ B ^ (p.natDegree - i) * p.natDegree.choose i :=
by
obtain hB | hB := lt_or_ge B 0
· rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero, one_mul, coeff_one]
split_ifs with h <;> simp [h]
rw [← h1.natDegree_map f]
obtain hi | hi := lt_or_ge (map f p).natDegree i
· rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
positivity
rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) hi, (h1.map _).leadingCoeff, one_mul, norm_mul,
norm_pow, norm_neg, norm_one, one_pow, one_mul]
apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
·
rw [Multiset.map_map, card_map, card_powersetCard, ← natDegree_eq_card_roots' h2, Nat.choose_symm hi, mul_comm,
nsmul_eq_mul]
intro r hr
simp_rw [Multiset.mem_map] at hr
obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
rw [mem_powersetCard] at hs
lift B to ℝ≥0 using hB
rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
MonoidHom.map_multiset_prod]
refine (prod_le_pow_card _ B fun x hx => ?_).trans_eq (by rw [card_map, hs.2])
obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
exact h3 z (mem_of_le hs.1 hz)
