The quotient by a Weierstrass polynomial

For a Weierstrass polynomial W ∈ (Conv K m)[X] (monic of degree d, lower coefficients vanishing at 0), P := convPolyEval W ∈ Conv K (m+1) is x_0-regular of order d (isRegularIn_convPolyEval_weierstrassPolynomial), and evaluation at x_0 induces a ring isomorphism (Conv K m)[X] ⧸ (W) ≃+* Conv K (m+1) ⧸ (P) (exists_ringEquiv_quotient_weierstrass, stated with the inverse direction and the compatibility e (mk (convPolyEval q)) = mk q): it is surjective because the Weierstrass division writes every element as q P + r with r of x_0-degree < d, and r is the evaluation of the polynomial of its slices; it is injective because a polynomial Q with convPolyEval Q ∈ (P) has remainder Q %ₘ W whose evaluation is both q' P + 0 and 0 · P + (itself), so by uniqueness of the division it vanishes, and convPolyEval is injective on polynomials (convPolyEval_injective: the x_0-slices of convPolyEval Q are the coefficients of Q). This is the convergent analogue of Mathlib's Polynomial.IsDistinguishedAt.algEquivQuotient for formal power series, and a standard step of the theory of [GR65, Chapter II, §B]; the unique factorization argument (UFD.lean) rests on it.

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.coe_convPolyEval_eq_sum {K : Type u_1} [RCLike K] {m : ℕ} (Q : Polynomial ↥(Conv K m)) : ↑((convPolyEval K) Q) = ∑ k ∈ Finset.range (Q.natDegree + 1), liftTail ↑(Q.coeff k) * MvPowerSeries.X 0 ^ k

convPolyEval Q as the finite sum of its terms.

theorem Analytic.coeff_splitFirst_convPolyEval {K : Type u_1} [RCLike K] {m : ℕ} (Q : Polynomial ↥(Conv K m)) (k : ℕ) : (PowerSeries.coeff k) ((splitFirst K m) ↑((convPolyEval K) Q)) = ↑(Q.coeff k)

The x_0-slices of convPolyEval Q are the coefficients of Q.

theorem Analytic.convPolyEval_injective {K : Type u_1} [RCLike K] {m : ℕ} : Function.Injective ⇑(convPolyEval K)

convPolyEval is injective.

theorem Analytic.coeff_convPolyEval_eq_zero_of_degree_lt {K : Type u_1} [RCLike K] {m : ℕ} {Q : Polynomial ↥(Conv K m)} {d : ℕ} (hQ : Q.degree < ↑d) {ν : Fin (m + 1) →₀ ℕ} (hν : d ≤ ν 0) : (MvPowerSeries.coeff ν) ↑((convPolyEval K) Q) = 0

A polynomial of degree < d evaluates to a series of x_0-degree < d.

theorem Analytic.coe_convPolyEval_weierstrassPolynomial {K : Type u_1} [RCLike K] {m : ℕ} (d : ℕ) (c : Fin d → ↥(Conv K m)) : ↑((convPolyEval K) (weierstrassPolynomial d c)) = weierstrassPoly d fun (j : Fin d) => ↑(c j)

convPolyEval sends the Weierstrass polynomial over Conv K m to the series weierstrassPoly.

theorem Analytic.isRegularIn_weierstrassPoly {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → MvPowerSeries (Fin m) K} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff (c j) = 0) : IsRegularIn (weierstrassPoly d c) d

A Weierstrass polynomial with coefficients vanishing at 0 is x_0-regular of order d (the printed condition μ_0(c_j) ≥ j of [BM88, proof of Theorem 4.4, p. 24, item (2)]).

theorem Analytic.isRegularIn_convPolyEval_weierstrassPolynomial {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) : IsRegularIn (↑((convPolyEval K) (weierstrassPolynomial d c))) d

theorem Analytic.exists_ringEquiv_quotient_weierstrass {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → ↥(Conv K m)} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff ↑(c j) = 0) : ∃ (e : ↥(Conv K (m + 1)) ⧸ Ideal.span {(convPolyEval K) (weierstrassPolynomial d c)} ≃+* Polynomial ↥(Conv K m) ⧸ Ideal.span {weierstrassPolynomial d c}), ∀ (q : Polynomial ↥(Conv K m)), e ((Ideal.Quotient.mk (Ideal.span {(convPolyEval K) (weierstrassPolynomial d c)})) ((convPolyEval K) q)) = (Ideal.Quotient.mk (Ideal.span {weierstrassPolynomial d c})) q

For a Weierstrass polynomial W over Conv K m, Conv K (m+1) ⧸ (W(x_0)) is isomorphic to (Conv K m)[X] ⧸ (W), compatibly with the evaluation at x_0 [GR65, Chapter II, §B] (the convergent analogue of Mathlib's Polynomial.IsDistinguishedAt.algEquivQuotient), from the convergent Weierstrass division.