Root bounds and root counts for distinguished polynomials

A monic polynomial distinguished in its full degree at a positive radius has all its roots in the corresponding closed disc. This uses only the Gauss-norm coefficient bounds, without Weierstrass division or preparation, and applies over ultrametric normed commutative rings with multiplicative norm, without completeness. It supplies the outer root bound for quotients of preparation polynomials at nested radii.

The polynomial root estimate is Polynomial.Monic.exists_apply_pow_le_apply_coeff_of_eval_eq_zero.

Over an ultrametric normed field the two dominant degrees of a nonzero polynomial P at a radius c > 0 count its roots, with multiplicity: the distinguished degree (the last index attaining the Gauss norm) bounds the number of roots in the closed disc ‖x‖ ≤ c, and the lowest dominant degree (the first such index) bounds the number in the open disc ‖x‖ < c. When P splits both bounds are equalities, so their difference counts the roots on the sphere ‖x‖ = c. The linear factor X - b has distinguished degree 1 or 0 according as ‖b‖ ≤ c or not, and lowest dominant degree 1 or 0 according as ‖b‖ < c or not; both degrees add under products, and the factor of P without roots contributes nonnegative degrees. No valuation, Newton polygon or completeness is involved; the counts in terms of the endpoints of a finite Newton face for a real additive valuation are Polynomial.card_filter_roots_lt_addValuation and Polynomial.card_filter_roots_le_addValuation.

Main results

• TauCeti.PowerSeries.IsDistinguished.norm_le_of_eval_eq_zero: the roots of a monic polynomial distinguished in its full degree lie in the closed disc.
• TauCeti.PowerSeries.gaussNorm_X_sub_C: the Gauss norm of X - b at c ≥ 0 is max c ‖b‖.
• TauCeti.PowerSeries.IsDistinguished.card_filter_roots_norm_le_le and TauCeti.PowerSeries.IsDistinguished.card_filter_roots_norm_le_eq: the distinguished degree bounds, and for a split polynomial equals, the number of roots in the closed disc.
• TauCeti.PowerSeries.IsLowestDominant.card_filter_roots_norm_lt_le and TauCeti.PowerSeries.IsLowestDominant.card_filter_roots_norm_lt_eq: the same for the lowest dominant degree and the open disc.
• TauCeti.PowerSeries.card_filter_roots_norm_eq_eq: for a split polynomial the difference of the two degrees is the number of roots on the sphere.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.2.
• M. Lazard, Les zéros d'une fonction analytique d'une variable sur un corps valué complet, Publications Mathématiques de l'IHÉS 14 (1962), §1.

theorem TauCeti.PowerSeries.IsDistinguished.norm_le_of_eval_eq_zero {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {P : Polynomial R} (hP : IsDistinguished c s ↑P) (hc : 0 < c) (hm : P.IsMonicOfDegree s) {x : R} (hx : Polynomial.eval x P = 0) : ‖x‖ ≤ c

Every root of a monic polynomial distinguished in its full degree lies in its closed disc. The coefficient ring need not be complete or a field.

@[simp]

theorem TauCeti.PowerSeries.gaussNorm_X_sub_C {R : Type u_2} [NormedRing R] [NormOneClass R] {c : ℝ} (hc : 0 ≤ c) (b : R) : PowerSeries.gaussNorm norm c (PowerSeries.X - PowerSeries.C b) = max c ‖b‖

The Gauss norm at a radius c ≥ 0 of the linear series X - b is max c ‖b‖. This is the power series counterpart of Polynomial.gaussNorm_X_sub_C, for a norm that need not be multiplicative.

theorem TauCeti.PowerSeries.isDistinguished_zero_X_sub_C {R : Type u_2} [NormedRing R] [NormOneClass R] {c : ℝ} (hc : 0 < c) {b : R} (hb : c < ‖b‖) : IsDistinguished c 0 (PowerSeries.X - PowerSeries.C b)

A linear polynomial X - b whose root lies outside the closed disc of radius c > 0 is distinguished of degree 0 at c: its Gauss norm ‖b‖ is attained only by the constant term.

theorem TauCeti.PowerSeries.isLowestDominant_zero_X_sub_C {R : Type u_2} [NormedRing R] [NormOneClass R] {c : ℝ} (hc : 0 < c) {b : R} (hb : c ≤ ‖b‖) : IsLowestDominant c 0 (PowerSeries.X - PowerSeries.C b)

A linear polynomial X - b whose root lies outside the open disc of radius c > 0 has lowest dominant degree 0 at c: its Gauss norm ‖b‖ is attained by the constant term.

theorem TauCeti.PowerSeries.isDistinguished_multiset_prod_X_sub_C {K : Type u_2} [NormedField K] {c : ℝ} [IsUltrametricDist K] (hc : 0 < c) (s : Multiset K) : IsDistinguished c (Multiset.filter (fun (x : K) => ‖x‖ ≤ c) s).card ↑(Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) s).prod

A product of linear factors ∏ (X - a) is distinguished at the radius c > 0 of degree the number of its roots in the closed disc of radius c, counted with multiplicity.

theorem TauCeti.PowerSeries.isLowestDominant_multiset_prod_X_sub_C {K : Type u_2} [NormedField K] {c : ℝ} [IsUltrametricDist K] (hc : 0 < c) (s : Multiset K) : IsLowestDominant c (Multiset.filter (fun (x : K) => ‖x‖ < c) s).card ↑(Multiset.map (fun (a : K) => Polynomial.X - Polynomial.C a) s).prod

A product of linear factors ∏ (X - a) has lowest dominant degree at the radius c > 0 the number of its roots in the open disc of radius c, counted with multiplicity.

theorem TauCeti.PowerSeries.IsDistinguished.card_filter_roots_norm_le_le {K : Type u_2} [NormedField K] {c : ℝ} {d : ℕ} {P : Polynomial K} [IsUltrametricDist K] (hP : IsDistinguished c d ↑P) (hc : 0 < c) : (Multiset.filter (fun (x : K) => ‖x‖ ≤ c) P.roots).card ≤ d

Roots in the closed disc. A polynomial over an ultrametric normed field distinguished of degree d at the radius c > 0 has at most d roots x with ‖x‖ ≤ c, counted with multiplicity.

theorem TauCeti.PowerSeries.IsDistinguished.card_filter_roots_norm_le_eq {K : Type u_2} [NormedField K] {c : ℝ} {d : ℕ} {P : Polynomial K} [IsUltrametricDist K] (hP : IsDistinguished c d ↑P) (hc : 0 < c) (hs : P.Splits) : (Multiset.filter (fun (x : K) => ‖x‖ ≤ c) P.roots).card = d

Roots in the closed disc of a split polynomial. A split polynomial over an ultrametric normed field distinguished of degree d at the radius c > 0 has exactly d roots x with ‖x‖ ≤ c, counted with multiplicity.

theorem TauCeti.PowerSeries.IsLowestDominant.card_filter_roots_norm_lt_le {K : Type u_2} [NormedField K] {c : ℝ} {l : ℕ} {P : Polynomial K} [IsUltrametricDist K] (hP : IsLowestDominant c l ↑P) (hc : 0 < c) : (Multiset.filter (fun (x : K) => ‖x‖ < c) P.roots).card ≤ l

Roots in the open disc. A polynomial over an ultrametric normed field with lowest dominant degree l at the radius c > 0 has at most l roots x with ‖x‖ < c, counted with multiplicity.

theorem TauCeti.PowerSeries.IsLowestDominant.card_filter_roots_norm_lt_eq {K : Type u_2} [NormedField K] {c : ℝ} {l : ℕ} {P : Polynomial K} [IsUltrametricDist K] (hP : IsLowestDominant c l ↑P) (hc : 0 < c) (hs : P.Splits) : (Multiset.filter (fun (x : K) => ‖x‖ < c) P.roots).card = l

Roots in the open disc of a split polynomial. A split polynomial over an ultrametric normed field with lowest dominant degree l at the radius c > 0 has exactly l roots x with ‖x‖ < c, counted with multiplicity.

theorem TauCeti.PowerSeries.card_filter_roots_norm_eq_eq {K : Type u_2} [NormedField K] {c : ℝ} {d l : ℕ} {P : Polynomial K} [IsUltrametricDist K] (hd : IsDistinguished c d ↑P) (hl : IsLowestDominant c l ↑P) (hc : 0 < c) (hs : P.Splits) : (Multiset.filter (fun (x : K) => ‖x‖ = c) P.roots).card = d - l

Roots on the sphere of a split polynomial. A split polynomial over an ultrametric normed field distinguished of degree d and with lowest dominant degree l at the radius c > 0 has exactly d - l roots x with ‖x‖ = c, counted with multiplicity.