English
Given a bound B for norms of images of x under all embeddings, each coefficient of the minimal polynomial of x over ℚ is bounded by a universal real expression in B and the finite rank of K over ℚ.
Русский
При заданном ограничении для норм образов x через все вложения, коэффициенты минимального многочлена x над ℚ ограничены выражением, зависящим от B и ранга поля.
LaTeX
$$$\forall i, \| (\minpoly_{\mathbb{Q}}(x)).\text{coeff} i \| \, \le \, \max(B,1)^{\operatorname{finrank}_{\mathbb{Q}}K} \cdot \binom{\operatorname{finrank}_{\mathbb{Q}}K}{\tfrac{\operatorname{finrank}_{\mathbb{Q}}K}{2}}^{\text{cast}}$$$
Lean4
theorem coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ‖φ x‖ ≤ B) (i : ℕ) :
‖(minpoly ℚ x).coeff i‖ ≤ max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2) :=
by
have hx := Algebra.IsSeparable.isIntegral ℚ x
rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
refine
coeff_bdd_of_roots_le _ (minpoly.monic hx) (IsAlgClosed.splits_codomain _) (minpoly.natDegree_le x) (fun z hz => ?_)
i
classical
rw [← Multiset.mem_toFinset] at hz
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
exact h φ
