Series of bounded x_0-degree as polynomials over the tail ring; division in Conv K (m+1)

A series r with coeff ν r = 0 whenever ν 0 ≥ d is ∑_{j<d} (x_0-slice j of r) · x_0^j, the slices being the coefficients of splitFirst m r (convergent when r is, coeff_splitFirst_mem_conv); in Conv K (m+1) this reads r = ∑_j convTail (sliceConv r j) * convX 0 ^ j (eq_sum_convTail_sliceConv). The convergent Weierstrass division is restated for elements of Conv K (m+1) (exists_division_conv): for g x_0-regular of order d, every f is q g + r with r of x_0-degree < d. These two facts make Conv K (m+1) ⧸ (g) a module generated by 1, x_0, …, x_0^{d-1} over Conv K m, the step of Rückert's basis theorem (Noetherian.lean) [GR65, Chapter II, §B].

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

theorem Analytic.eq_sum_liftTail_coeff_splitFirst {K : Type u_1} [RCLike K] {m : ℕ} {r : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hr : ∀ (ν : Fin (m + 1) →₀ ℕ), d ≤ ν 0 → (MvPowerSeries.coeff ν) r = 0) : r = ∑ j : Fin d, liftTail ((PowerSeries.coeff (d - 1 - ↑j)) ((splitFirst K m) r)) * MvPowerSeries.X 0 ^ (d - 1 - ↑j)

A series of x_0-degree < d is the sum of its x_0-slices times powers of x_0.

noncomputable def Analytic.sliceConv {K : Type u_1} [RCLike K] {m : ℕ} (r : ↥(Conv K (m + 1))) (k : ℕ) : ↥(Conv K m)

The x_0-slices of a convergent series, as elements of Conv K m (coeff_splitFirst_mem_conv).

Equations

• Analytic.sliceConv r k = ⟨(PowerSeries.coeff k) ((Analytic.splitFirst K m) ↑r), ⋯⟩

@[simp]

theorem Analytic.coe_sliceConv {K : Type u_1} [RCLike K] {m : ℕ} (r : ↥(Conv K (m + 1))) (k : ℕ) : ↑(sliceConv r k) = (PowerSeries.coeff k) ((splitFirst K m) ↑r)

theorem Analytic.eq_sum_convTail_sliceConv {K : Type u_1} [RCLike K] {m : ℕ} {r : ↥(Conv K (m + 1))} {d : ℕ} (hr : ∀ (ν : Fin (m + 1) →₀ ℕ), d ≤ ν 0 → (MvPowerSeries.coeff ν) ↑r = 0) : r = ∑ j : Fin d, (convTail K) (sliceConv r (d - 1 - ↑j)) * convX K 0 ^ (d - 1 - ↑j)

In Conv K (m+1), a series of x_0-degree < d is ∑_j convTail (slice_j) * x_0^j.

theorem Analytic.exists_division_conv {K : Type u_1} [RCLike K] {m : ℕ} {f g : ↥(Conv K (m + 1))} {d : ℕ} (hreg : IsRegularIn (↑g) d) : ∃ (q : ↥(Conv K (m + 1))) (r : ↥(Conv K (m + 1))), (∀ (ν : Fin (m + 1) →₀ ℕ), d ≤ ν 0 → (MvPowerSeries.coeff ν) ↑r = 0) ∧ f = q * g + r

The convergent Weierstrass division for elements of Conv K (m+1).