Weierstrass polynomials: coefficients, order, and the polynomial over the tail ring #
A Weierstrass polynomial x_0^d + ∑_{j<d} c_j(x') x_0^{d-1-j} (weierstrassPoly, a series in
m + 1 variables) corresponds under splitFirst K m to the polynomial X^d + ∑ C(c_j) X^{d-1-j}
over the tail ring (weierstrassPolynomial, defined over any commutative ring), which is monic of
degree d, and distinguished
when the c_j vanish at 0. Its coefficients are read off exponent by exponent
(coeff_cons_weierstrassPoly): the terms have distinct x_0-degrees, so there is no
cancellation, and the order is d exactly when μ_0(c_j) ≥ j + 1 for every j; since our c_j
is the printed c_{j+1}, this is the printed condition μ_0(c_j) ≥ j on the coefficients
[BM88, proof of Theorem 4.4, p. 24, item (2)]. A series of x_0-degree < d is its own
truncation, hence a polynomial of degree < d over the tail ring: this is how the convergent
remainders enter Mathlib's IsWeierstrassDivision.
The coefficient field K is ℝ or ℂ ([RCLike K]).
Coefficients of lifted series and Weierstrass polynomials #
The coefficient of x_0^k x'^x in a Weierstrass polynomial: the terms have distinct
x_0-degrees, so the coefficient is read off term by term.
The order of a Weierstrass polynomial #
μ_0(P) ≤ d, the coefficient of x_0^d being 1.
μ_0(P) = d iff μ_0(c_j) ≥ j + 1 for all j (no cancellation between terms of distinct
x_0-degree): the printed μ_0(c_j) ≥ j of [BM88, proof of Theorem 4.4, p. 24, item (2)], our
c_j being the printed c_{j+1}.
The polynomial over the tail ring #
The polynomial weierstrassPolynomial d c is defined over an arbitrary commutative ring; here it is
compared with the series weierstrassPoly d c through splitFirst.
Under splitFirst, the Weierstrass polynomial in m + 1 variables is the polynomial over the
tail ring.
A Weierstrass polynomial whose coefficients vanish at 0 is distinguished at the maximal
ideal of the tail ring (monic, lower coefficients in 𝔪).
Series of bounded x_0-degree are polynomials over the tail ring #
x_0^d - r, for r of x_0-degree < d, is the Weierstrass polynomial with coefficients
the negated x_0-coefficients of r.
A convergent-style division datum f = q g + r, r of x_0-degree < d, is a Weierstrass
division in Mathlib's sense over the tail ring.
The toNat of the order of the residue image of a regular series is its regularity order.