The contraction step of Weierstrass division

For the normalized divisor x_0^d - h with ‖h‖_ρ ≤ ρ_0^d / 2, dividing f ∈ B_ρ amounts to solving f + h q = x_0^d q + r with r of x_0-degree < d; applying the splitting operators, q = Q(f) + Q(h q) and r = R(f + h q). The map T q := Q f + Q (h q) is a contraction of B_ρ with constant ‖Q‖ ‖h‖ ≤ ρ_0^{-d} · ρ_0^d / 2 = 1/2 (the operator bounds of Splitting.lean), so it has a fixed point q in the Banach space B_ρ (ContractingWith.fixedPoint), and f = q (x_0^d - h) + R(f + h q). This is the Banach-algebra proof of the Weierstrass division theorem [GR71, Kapitel I]; Division.lean removes the normalization and the smallness hypothesis.

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

theorem Analytic.exists_division_of_convNorm_le {K : Type u_1} [RCLike K] {m : ℕ} (ρ : Radius (m + 1)) (d : ℕ) {f h : MvPowerSeries (Fin (m + 1)) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) (hh : ConvNorm (↑ρ) h ≤ ↑(↑ρ 0 ^ d / 2)) : ∃ (q : MvPowerSeries (Fin (m + 1)) K) (r : MvPowerSeries (Fin (m + 1)) K), ConvNorm (↑ρ) q ≠ ⊤ ∧ ConvNorm (↑ρ) r ≠ ⊤ ∧ (∀ (ν : Fin (m + 1) →₀ ℕ), d ≤ ν 0 → (MvPowerSeries.coeff ν) r = 0) ∧ f = q * (MvPowerSeries.X 0 ^ d - h) + r

The contraction step: for g = x_0^d - h with ‖h‖_ρ ≤ ρ_0^d / 2, every f ∈ B_ρ is q g + r with q, r ∈ B_ρ and r of x_0-degree < d [GR71, Kapitel I].