Normalization of a regular series

A convergent g, x_0-regular of order d, is e(x_0) · (x_0^d - h) with e a convergent unit in x_0 alone and h without pure x_0-terms. The restriction of g to the axis is x_0^d · e where e := axis (wQ d g) (the pure x_0-coefficients of g below degree d vanish, so axis (wR d g) = 0), and e(0) is the x_0^d-coefficient of g, nonzero by regularity. With E := liftFirst e, a unit of Conv K (m + 1) because its constant term is nonzero, put h := x_0^d - E⁻¹ g: its restriction to the axis is x_0^d - axis E⁻¹ · x_0^d e = 0, and g = E (x_0^d - h). This is the reduction to a divisor of the form x_0^d - h in the Banach-algebra proof of Weierstrass division [GR71, Kapitel I]; the smallness of h is arranged in Division.lean by shrinking the tail radii.

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

theorem Analytic.wQ_mem_conv {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} (hg : g ∈ Conv K (m + 1)) (d : ℕ) : wQ d g ∈ Conv K (m + 1)

theorem Analytic.tailVanishes_iff_axis_eq_zero {K : Type u_1} [RCLike K] {m : ℕ} (h : MvPowerSeries (Fin (m + 1)) K) : TailVanishes h ↔ axis h = 0

theorem Analytic.axis_wR_eq_zero {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hg : ∀ k < d, (MvPowerSeries.coeff (Finsupp.single 0 k)) g = 0) : axis (wR d g) = 0

For g with vanishing pure x_0-coefficients below d, the remainder part wR d g has no pure x_0-terms.

theorem Analytic.axis_eq_X_pow_mul {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hg : ∀ k < d, (MvPowerSeries.coeff (Finsupp.single 0 k)) g = 0) : axis g = MvPowerSeries.X 0 ^ d * axis (wQ d g)

g(x_0, 0) = x_0^d · e(x_0) with e = axis (wQ d g).

theorem Analytic.IsRegularIn.exists_normalized {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hg : g ∈ Conv K (m + 1)) (hreg : IsRegularIn g d) : ∃ (e : MvPowerSeries (Fin 1) K) (h : MvPowerSeries (Fin (m + 1)) K), e ∈ Conv K 1 ∧ MvPowerSeries.constantCoeff e ≠ 0 ∧ h ∈ Conv K (m + 1) ∧ TailVanishes h ∧ g = liftFirst e * (MvPowerSeries.X 0 ^ d - h)

Normalization: a convergent g, x_0-regular of order d, is e(x_0) · (x_0^d - h) with e a convergent unit in x_0 alone and h without pure x_0-terms.