Convergent Weierstrass preparation

The Weierstrass preparation theorem for convergent power series [GR65, Chapter II, §B], in the form Bierstone and Milman quote it [BM88, proof of Theorem 4.4, p. 24]: a convergent g, x_0-regular of order d, is u · (x_0^d + ∑_{j<d} c_j x_0^{d-1-j}) with u a convergent unit and convergent c_j in the tail variables vanishing at 0, uniquely. Divide x_0^d by g (Division.lean): x_0^d = q g + r with r of x_0-degree < d. Mathlib's formal argument (IsWeierstrassDivision.isUnit_of_map_ne_zero) shows q is a unit; its inverse u is convergent (Hironaka/Analytic/ConvSeries/Units.lean), and g = u (x_0^d - r) where x_0^d - r is the Weierstrass polynomial with coefficients c_j = -(x_0^{d-1-j}-coefficient of r), convergent (Tail.lean) and vanishing at 0 (restrict x_0^d = q g + r to the axis: axis r = x_0^d (1 - axis q · e) has no terms below degree d). Uniqueness: a datum g = u' P' with P' a Weierstrass polynomial whose coefficients vanish at 0 is a Weierstrass factorization in Mathlib's sense (u' is a unit since its constant term is the x_0^d-coefficient of g), and IsWeierstrassFactorization.elim applies.

This is the local form behind the coherence of the structure sheaf of an analytic space (Hironaka/AnalyticSpace/Oka); FunctionLevel.lean turns it into a statement about analytic functions on a product polydisc.

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

theorem Analytic.coeff_single_eq_zero_of_X_pow_eq {K : Type u_1} [RCLike K] {m : ℕ} {g q r : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hlow : ∀ k < d, (MvPowerSeries.coeff (Finsupp.single 0 k)) g = 0) (hXq : MvPowerSeries.X 0 ^ d = q * g + r) {k : ℕ} (hk : k < d) : (MvPowerSeries.coeff (Finsupp.single 0 k)) r = 0

Restricting x_0^d = q g + r to the axis: r has no pure x_0-terms below degree d.

theorem Analytic.axis_weierstrassPoly {K : Type u_1} [RCLike K] {m d : ℕ} {c : Fin d → MvPowerSeries (Fin m) K} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff (c j) = 0) : axis (weierstrassPoly d c) = MvPowerSeries.X 0 ^ d

The restriction to the axis of a Weierstrass polynomial with coefficients vanishing at 0 is x_0^d.

theorem Analytic.coeff_single_of_mul_weierstrassPoly {K : Type u_1} [RCLike K] {m : ℕ} {g u' : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} {c' : Fin d → MvPowerSeries (Fin m) K} (hc' : ∀ (j : Fin d), MvPowerSeries.constantCoeff (c' j) = 0) (hg : g = u' * weierstrassPoly d c') : (MvPowerSeries.coeff (Finsupp.single 0 d)) g = MvPowerSeries.constantCoeff u'

If g = u' P' with P' a Weierstrass polynomial whose coefficients vanish at 0, the x_0^d-coefficient of g is the constant term of u'.

theorem Analytic.isWeierstrassFactorization_of_eq {K : Type u_1} [RCLike K] {m : ℕ} {g u : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} {c : Fin d → MvPowerSeries (Fin m) K} (hc : ∀ (j : Fin d), MvPowerSeries.constantCoeff (c j) = 0) (hu : MvPowerSeries.constantCoeff u ≠ 0) (hg : g = u * weierstrassPoly d c) : ((splitFirst K m) g).IsWeierstrassFactorization (weierstrassPolynomial d c) ((splitFirst K m) u)

A factorization g = u P with P a Weierstrass polynomial with coefficients vanishing at 0 and u(0) ≠ 0 is a Weierstrass factorization over the tail ring.

theorem Analytic.exists_unique_weierstrassPreparation {K : Type u_1} [RCLike K] {m : ℕ} {g : MvPowerSeries (Fin (m + 1)) K} {d : ℕ} (hg : g ∈ Conv K (m + 1)) (hreg : IsRegularIn g d) : ∃ (u : MvPowerSeries (Fin (m + 1)) K) (c : Fin d → MvPowerSeries (Fin m) K), u ∈ Conv K (m + 1) ∧ MvPowerSeries.constantCoeff u ≠ 0 ∧ (∀ (j : Fin d), c j ∈ Conv K m ∧ MvPowerSeries.constantCoeff (c j) = 0) ∧ g = u * weierstrassPoly d c ∧ ∀ (u' : MvPowerSeries (Fin (m + 1)) K) (c' : Fin d → MvPowerSeries (Fin m) K), (∀ (j : Fin d), MvPowerSeries.constantCoeff (c' j) = 0) → g = u' * weierstrassPoly d c' → u' = u ∧ c' = c

Convergent Weierstrass preparation: g = u · (x_0^d + ∑_{j<d} c_j x_0^{d-1-j}) with u a convergent unit and convergent c_j vanishing at 0, uniquely [GR65, Chapter II, §B]; the form quoted in [BM88, proof of Theorem 4.4, p. 24].