Convergent Weierstrass division

The Weierstrass division theorem for convergent power series [GR65, Chapter II, §B], [Nar66, Chapter II, Theorem 2]: for convergent f, g with g x_0-regular of order d, there are unique convergent q, r with f = q g + r and r of x_0-degree < d. Existence follows the Banach-algebra argument [GR71, Kapitel I]: normalize g = E (x_0^d - h) (Normalize.lean), pick a radius vector where f and h converge, shrink its tail so that ‖h‖_ρ ≤ ρ_0^d / 2 (Splitting.lean), divide by the contraction (Contraction.lean), f = q₁ (x_0^d - h) + r, and put q := q₁ E⁻¹. Uniqueness: a convergent division datum is a formal Weierstrass division over the tail ring (isWeierstrassDivision_of_eq in Poly.lean), and Mathlib's formal uniqueness (PowerSeries.IsWeierstrassDivision.elim) applies. The preparation theorem of Preparation.lean is the division of x_0^d by g.

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

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

Uniqueness of Weierstrass division data, from the formal theorem.

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

Convergent Weierstrass division: unique convergent q, r with f = q g + r and r of x_0-degree < d [GR65, Chapter II, §B], [Nar66, Chapter II, Theorem 2].