Roots of monic polynomials under power-multiplicative seminorms

Let f be a nonarchimedean, power-multiplicative ring seminorm on a ring R, and let x : R be a root of a monic polynomial p = X ^ d + ∑_{i < d} aᵢ X ^ i over R itself. Then f x is controlled by the coefficients: some i < d satisfies f x ^ (d - i) ≤ f aᵢ, and hence

f x ≤ max_{i < d} f aᵢ ^ (1 / (d - i)).

This is the ring-seminorm form of the bound of the norm of a root by the spectral value of a polynomial, norm_root_le_spectralValue, which treats coefficients in a normed field and roots in an algebra over it. Here the coefficients and the root live in the same ring, as in the integral equations used to bound supremum seminorms of affinoid algebras.

Conversely, if p has d roots in a domain, counted with multiplicity, then each coefficient is bounded by the largest root: f aᵢ ≤ M ^ (d - i) whenever f a ≤ M for every root a. Together the two bounds identify max_{i < d} f aᵢ ^ (1 / (d - i)) with the largest value of f on the roots of a split monic polynomial. This adapts the second half of the proof of Mathlib's max_norm_root_eq_spectralValue ([BGR] §3.1.2, Proposition 1(2)) to ring seminorms.

Bounds of the form f aᵢ ≤ M ^ (d - i) are also stable under products and powers of polynomials, since each coefficient of a product is a sum of products of coefficients.

Main results

• Polynomial.Monic.exists_apply_pow_le_apply_coeff_of_eval_eq_zero: some i < d satisfies f x ^ (d - i) ≤ f aᵢ.
• Polynomial.Monic.apply_le_iSup_apply_coeff_rpow_of_eval_eq_zero: f x ≤ ⨆ i < d, f aᵢ ^ (1 / (d - i)).
• Multiset.apply_esymm_le_pow: f (s.esymm k) ≤ M ^ k when f a ≤ M on s and k ≤ card s.
• Polynomial.Monic.apply_coeff_le_pow_of_card_roots: f aᵢ ≤ M ^ (d - i) when p has d roots, all with f-value at most M.
• Polynomial.apply_coeff_mul_le_pow, Polynomial.apply_coeff_prod_le_pow, Polynomial.apply_coeff_pow_le_pow: the bounds f aᵢ ≤ M ^ (d - i) pass to products and powers.

References

• [Bosch, Güntzer, Remmert, Non-Archimedean Analysis][bosch-guntzer-remmert], §3.1.2 (Proposition 1) and §3.8.1.

theorem Polynomial.Monic.exists_apply_pow_le_apply_coeff_of_eval_eq_zero {R : Type u_1} {F : Type u_2} [Ring R] [FunLike F R ℝ] [RingSeminormClass F R ℝ] {f : F} {p : Polynomial R} {x : R} [Nontrivial R] (hp : p.Monic) (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hx : eval x p = 0) : ∃ i < p.natDegree, f x ^ (p.natDegree - i) ≤ f (p.coeff i)

A root x of a monic polynomial p of degree d over a nontrivial ring satisfies f x ^ (d - i) ≤ f (p.coeff i) for some i < d, for every nonarchimedean power-multiplicative ring seminorm f.

theorem Polynomial.Monic.apply_le_iSup_apply_coeff_rpow_of_eval_eq_zero {R : Type u_1} {F : Type u_2} [Ring R] [FunLike F R ℝ] [RingSeminormClass F R ℝ] {f : F} {p : Polynomial R} {x : R} (hp : p.Monic) (hf_pm : IsPowMul ⇑f) (hf_na : IsNonarchimedean ⇑f) (hx : eval x p = 0) : f x ≤ ⨆ (i : Fin p.natDegree), f (p.coeff ↑i) ^ (1 / (↑p.natDegree - ↑↑i))

Root bound for monic polynomials. A root x of a monic polynomial p of degree d satisfies f x ≤ ⨆ i < d, f (p.coeff i) ^ (1 / (d - i)), for every nonarchimedean power-multiplicative ring seminorm f.

theorem Multiset.apply_esymm_le_pow {R : Type u_1} {F : Type u_2} [CommRing R] [FunLike F R ℝ] [RingSeminormClass F R ℝ] {f : F} (hf1 : f 1 ≤ 1) (hf_na : IsNonarchimedean ⇑f) {s : Multiset R} {M : ℝ} (hM : ∀ a ∈ s, f a ≤ M) {k : ℕ} (hk : k ≤ s.card) : f (s.esymm k) ≤ M ^ k

The elementary symmetric functions of a multiset are bounded by powers of a bound on its elements: if f a ≤ M for every a ∈ s, then f (s.esymm k) ≤ M ^ k for every k up to the cardinality of s, for every nonarchimedean ring seminorm f with f 1 ≤ 1. This adapts the coefficient half of the proof of Mathlib's max_norm_root_eq_spectralValue ([BGR] §3.1.2, Proposition 1(2)).

theorem Polynomial.Monic.apply_coeff_le_pow_of_card_roots {R : Type u_1} {F : Type u_2} [CommRing R] [FunLike F R ℝ] [RingSeminormClass F R ℝ] {f : F} [IsDomain R] {p : Polynomial R} (hp : p.Monic) (hf1 : f 1 ≤ 1) (hf_na : IsNonarchimedean ⇑f) (hroots : p.roots.card = p.natDegree) {M : ℝ} (hM : ∀ a ∈ p.roots, f a ≤ M) (i : ℕ) : f (p.coeff i) ≤ M ^ (p.natDegree - i)

Coefficients are bounded by the roots. If a monic polynomial p of degree d over a domain has d roots counted with multiplicity, and f a ≤ M for every root a, then f (p.coeff i) ≤ M ^ (d - i) for every i, for every nonarchimedean ring seminorm f with f 1 ≤ 1. This complements Polynomial.Monic.apply_le_iSup_apply_coeff_rpow_of_eval_eq_zero.

theorem Polynomial.apply_coeff_mul_le_pow {R : Type u_1} {F : Type u_2} [FunLike F R ℝ] {f : F} {M : ℝ} [Ring R] [RingSeminormClass F R ℝ] (hf_na : IsNonarchimedean ⇑f) {p q : Polynomial R} {d e : ℕ} (hpd : p.natDegree ≤ d) (hqe : q.natDegree ≤ e) (hp : ∀ (i : ℕ), f (p.coeff i) ≤ M ^ (d - i)) (hq : ∀ (i : ℕ), f (q.coeff i) ≤ M ^ (e - i)) (k : ℕ) : f ((p * q).coeff k) ≤ M ^ (d + e - k)

Coefficient bounds multiply. If f (p.coeff i) ≤ M ^ (d - i) for a polynomial p of degree at most d, and f (q.coeff i) ≤ M ^ (e - i) for q of degree at most e, then f ((p * q).coeff k) ≤ M ^ (d + e - k), for every nonarchimedean ring seminorm f.

theorem Polynomial.apply_coeff_pow_le_pow {R : Type u_1} {F : Type u_2} [FunLike F R ℝ] {f : F} {M : ℝ} [Ring R] [RingSeminormClass F R ℝ] (hf1 : f 1 ≤ 1) (hf_na : IsNonarchimedean ⇑f) {p : Polynomial R} (hp : ∀ (i : ℕ), f (p.coeff i) ≤ M ^ (p.natDegree - i)) (n k : ℕ) : f ((p ^ n).coeff k) ≤ M ^ (n * p.natDegree - k)

Coefficient bounds f (p.coeff i) ≤ M ^ (p.natDegree - i) pass to powers, for every nonarchimedean ring seminorm f with f 1 ≤ 1.

theorem Polynomial.apply_coeff_prod_le_pow {R : Type u_1} {F : Type u_2} [FunLike F R ℝ] {f : F} {M : ℝ} [CommRing R] [RingSeminormClass F R ℝ] (hf1 : f 1 ≤ 1) (hf_na : IsNonarchimedean ⇑f) {ι : Type u_3} (s : Finset ι) (p : ι → Polynomial R) (hp : ∀ a ∈ s, ∀ (i : ℕ), f ((p a).coeff i) ≤ M ^ ((p a).natDegree - i)) (k : ℕ) : f ((∏ a ∈ s, p a).coeff k) ≤ M ^ (∑ a ∈ s, (p a).natDegree - k)

Coefficient bounds f (p.coeff i) ≤ M ^ (p.natDegree - i) pass to finite products, for every nonarchimedean ring seminorm f with f 1 ≤ 1.