Dividing by a monic polynomial in the first variable

A monic polynomial p ∈ 𝒪_m[T] evaluated at the first variable, W = p(x_0) = convPolyEval p, is x_0-regular of some order d' ≤ deg p: the order of p(x_0, 0, …, 0) = x_0^{deg p} + ∑ p_k(0) x_0^k, a nonzero polynomial in one variable (IsRegularIn, in the coefficient form isRegularIn_iff). Weierstrass division by W (exists_division_conv, eq_sum_convTail_sliceConv of Slices.lean) then writes every G ∈ 𝒪_{m+1} as q W + ∑_{k < d'} b_k(x_1, …, x_m) x_0^k with convergent b_k: the remainder is a polynomial in x_0 of degree < d' ≤ deg p with coefficients in the tail ring 𝒪_m. This is the one-variable step of the iterated division of FibreDivision.lean (the division argument of [Fre17, Ch. I, 8.3]); the monic relations of the fibre coordinates need not be Weierstrass polynomials (their lower coefficients may have nonzero constant terms), which is why the order d' is not deg p in general.

theorem Analytic.single_zero_eq_cons {m : ℕ} (k : ℕ) : Finsupp.single 0 k = Finsupp.cons k 0

The exponent k in the first variable, as a Finsupp.cons.

theorem Analytic.coeff_single_zero_convPolyEval {K : Type u_1} [RCLike K] {m : ℕ} (p : Polynomial ↥(Conv K m)) (j : ℕ) : (MvPowerSeries.coeff (Finsupp.single 0 j)) ↑((convPolyEval K) p) = MvPowerSeries.constantCoeff ↑(p.coeff j)

The coefficient of x_0^j (with no other variable) in p(x_0) = convPolyEval p is the constant term of the j-th coefficient of p.

theorem Analytic.exists_isRegularIn_convPolyEval_of_monic {K : Type u_1} [RCLike K] {m : ℕ} (p : Polynomial ↥(Conv K m)) (hp : p.Monic) : ∃ d' ≤ p.natDegree, IsRegularIn (↑((convPolyEval K) p)) d'

A monic polynomial in x_0 with coefficients in the tail ring is x_0-regular of some order d' ≤ deg p: p(x_0, 0, …, 0) is a nonzero polynomial in one variable (its leading coefficient is 1), and d' is its order of vanishing at 0.

theorem Analytic.exists_eq_mul_add_sum_convTail_mul_convX_pow {K : Type u_1} [RCLike K] {m : ℕ} {W : ↥(Conv K (m + 1))} {d' : ℕ} (hreg : IsRegularIn (↑W) d') (G : ↥(Conv K (m + 1))) : ∃ (q : ↥(Conv K (m + 1))) (b : Fin d' → ↥(Conv K m)) (k : Fin d' → ℕ), (∀ (j : Fin d'), k j < d') ∧ G = q * W + ∑ j : Fin d', (convTail K) (b j) * convX K 0 ^ k j

Weierstrass division by an x_0-regular series W of order d' with the remainder written as a polynomial in x_0 of degree < d' whose coefficients are convergent series in the tail variables (eq_sum_convTail_sliceConv).