Weierstrass polynomials

A Weierstrass polynomial of degree s at a radius c > 0 is a monic polynomial p of degree s which, read as a restricted power series, is distinguished of degree s at c (TauCeti.PowerSeries.IsDistinguished). These are the polynomials produced by Weierstrass preparation, and the divisors for which Weierstrass division of restricted series reduces to polynomial division with remainder.

This file characterises Weierstrass polynomials by their coefficients and by their Gauss norm: p is one exactly when every weighted coefficient ‖pₖ‖ cᵏ is at most cˢ, the weight of the leading term, or equivalently when the Gauss norm of p at c is cˢ. At the unit radius these say that every coefficient of p has norm at most one, and that p has Gauss norm one.

Over a ring with an ultrametric norm, Weierstrass polynomials are closed under products (TauCeti.PowerSeries.IsDistinguished.mul). If the norm is also multiplicative, as for a Tate algebra over a complete nonarchimedean field, they are closed under taking monic factors: a monic polynomial of degree s has Gauss norm at least cˢ, so a product of two monic polynomials has Gauss norm cˢ exactly when both factors do. Multiplicativity of the norm cannot be dropped here. Over the dual numbers K[ε] of a nonarchimedean field K, with the norm ‖x + yε‖ = max ‖x‖ (C ‖y‖) for some C > 1, the product (X - ε) * (X + ε) = X ^ 2 is a Weierstrass polynomial at the unit radius, but X - ε is not.

Main results

• TauCeti.PowerSeries.isDistinguished_iff_of_isMonicOfDegree: a monic polynomial of degree s is distinguished of degree s at c > 0 iff ‖pₖ‖ cᵏ ≤ cˢ for every k < s.
• TauCeti.PowerSeries.pow_le_gaussNorm_of_isMonicOfDegree: a monic polynomial of degree s has Gauss norm at least cˢ.
• TauCeti.PowerSeries.isDistinguished_iff_gaussNorm_eq_of_isMonicOfDegree: it is distinguished of degree s iff its Gauss norm is cˢ.
• TauCeti.PowerSeries.isDistinguished_one_iff_of_isMonicOfDegree: at the unit radius, it is distinguished iff all its coefficients have norm at most one.
• TauCeti.PowerSeries.isDistinguished_mul_iff_of_isMonicOfDegree: for a multiplicative ultrametric norm, a product of monic polynomials is a Weierstrass polynomial iff both factors are.
• TauCeti.PowerSeries.IsDistinguished.of_dvd: for a multiplicative ultrametric norm, every monic factor of a Weierstrass polynomial is a Weierstrass polynomial.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.1 (Weierstrass polynomials) and §5.2.6.

theorem TauCeti.PowerSeries.isDistinguished_iff_of_isMonicOfDegree {R : Type u_1} [SeminormedRing R] [NormOneClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} (hc : 0 < c) (hp : p.IsMonicOfDegree s) : IsDistinguished c s ↑p ↔ ∀ k < s, ‖p.coeff k‖ * c ^ k ≤ c ^ s

A monic polynomial of degree s is distinguished of degree s at a radius c > 0 iff each of its lower weighted coefficients ‖pₖ‖ cᵏ is at most cˢ, the weight of its leading term.

theorem TauCeti.PowerSeries.isDistinguished_one_iff_of_isMonicOfDegree {R : Type u_1} [SeminormedRing R] [NormOneClass R] {s : ℕ} {p : Polynomial R} (hp : p.IsMonicOfDegree s) : IsDistinguished 1 s ↑p ↔ ∀ (k : ℕ), ‖p.coeff k‖ ≤ 1

At the unit radius, a monic polynomial of degree s is distinguished of degree s iff all of its coefficients have norm at most one.

theorem TauCeti.PowerSeries.pow_le_gaussNorm_of_isMonicOfDegree {R : Type u_1} [NormedRing R] [NormOneClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} (hp : p.IsMonicOfDegree s) : c ^ s ≤ PowerSeries.gaussNorm norm c ↑p

A monic polynomial of degree s has Gauss norm at least cˢ at every radius c: its leading term already has weighted norm cˢ.

theorem TauCeti.PowerSeries.isDistinguished_iff_gaussNorm_eq_of_isMonicOfDegree {R : Type u_1} [NormedRing R] [NormOneClass R] {c : ℝ} {s : ℕ} {p : Polynomial R} (hc : 0 < c) (hp : p.IsMonicOfDegree s) : IsDistinguished c s ↑p ↔ PowerSeries.gaussNorm norm c ↑p = c ^ s

A monic polynomial of degree s is distinguished of degree s at a radius c > 0 iff its Gauss norm at c is cˢ.

theorem TauCeti.PowerSeries.isDistinguished_mul_iff_of_isMonicOfDegree {R : Type u_1} [NormedRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {i j : ℕ} {p q : Polynomial R} (hc : 0 < c) (hp : p.IsMonicOfDegree i) (hq : q.IsMonicOfDegree j) : IsDistinguished c (i + j) (↑p * ↑q) ↔ IsDistinguished c i ↑p ∧ IsDistinguished c j ↑q

For a multiplicative ultrametric norm, a product of monic polynomials of degrees i and j is distinguished of degree i + j at a radius c > 0 iff each factor is distinguished of its degree.

theorem TauCeti.PowerSeries.IsDistinguished.of_dvd {R : Type u_1} [NormedRing R] [IsUltrametricDist R] [NormMulClass R] {c : ℝ} {s : ℕ} {p w : Polynomial R} (hw : IsDistinguished c s ↑w) (hc : 0 < c) (hwm : w.IsMonicOfDegree s) (hp : p.Monic) (hpw : p ∣ w) : IsDistinguished c p.natDegree ↑p

For a multiplicative ultrametric norm, a monic factor p of a monic polynomial w of degree s which is distinguished of degree s at a radius c > 0 is distinguished of its own degree at c: monic factors of Weierstrass polynomials are Weierstrass polynomials.