Function-level Weierstrass preparation on a product polydisc

An analytic f near 0 ∈ K^{m+1} whose restriction to the x_0-axis is t^d · e(t) with e(0) ≠ 0 (the printed f(0, …, 0, x_m) ∼ x_m^d) is the function of a convergent series F (Hironaka/Analytic/ConvSeries/Bridge.lean); the restriction of F to the axis is x_0^d E with E the series of e (uniqueness of the coefficients of a one-variable series), so F is x_0-regular of order d. Convergent preparation (Preparation.lean) gives F = U · (x_0^d + ∑ c_j x_0^{d-1-j}); on a polydisc where all the series converge and the sum of U does not vanish, evaluation is multiplicative and additive, which gives the product form f = u · P on V × D with which Bierstone and Milman open their proof ("By the Weierstrass preparation theorem, we can assume that U = V × D", [BM88, proof of Theorem 4.4, p. 24]).

This function-level form is the one used by the Taylor expansion of germs on a manifold (Hironaka/Manifold/Germ) and by the local models of Oka's coherence theorem (Hironaka/AnalyticSpace/Oka).

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

Evaluation of monomials, sums, lifts and axis restrictions

theorem Analytic.evalSeries_add {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {f g : MvPowerSeries (Fin m) K} (hf : ConvNorm (↑ρ) f ≠ ⊤) (hg : ConvNorm (↑ρ) g ≠ ⊤) {x : Fin m → K} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(↑ρ k)) : evalSeries (f + g) x = evalSeries f x + evalSeries g x

theorem Analytic.evalSeries_sum {K : Type u_1} [RCLike K] {m : ℕ} {ρ : Radius m} {ι : Type u_2} (s : Finset ι) {F : ι → MvPowerSeries (Fin m) K} (hF : ∀ i ∈ s, ConvNorm (↑ρ) (F i) ≠ ⊤) {x : Fin m → K} (hx : ∀ (k : Fin m), ‖x k‖ ≤ ↑(↑ρ k)) : evalSeries (∑ i ∈ s, F i) x = ∑ i ∈ s, evalSeries (F i) x

theorem Analytic.evalSeries_liftTail {K : Type u_1} [RCLike K] {m : ℕ} (a : MvPowerSeries (Fin m) K) (x : Fin (m + 1) → K) : evalSeries (liftTail a) x = evalSeries a (Fin.tail x)

Evaluating a lifted tail series forgets the first coordinate.

theorem Analytic.monomialEval_pi_single {K : Type u_1} [RCLike K] {m : ℕ} (t : K) (ν : Fin (m + 1) →₀ ℕ) : monomialEval (Pi.single 0 t) ν = if ν = Finsupp.single 0 (ν 0) then t ^ ν 0 else 0

theorem Analytic.evalSeries_axis {K : Type u_1} [RCLike K] {m : ℕ} (F : MvPowerSeries (Fin (m + 1)) K) (y : Fin 1 → K) : evalSeries (axis F) y = evalSeries F (Pi.single 0 (y 0))

Evaluating the axis restriction is evaluating on the axis.

Regularity from the axis restriction

theorem Analytic.isRegularIn_of_axis_eq {K : Type u_1} [RCLike K] {m : ℕ} {F : MvPowerSeries (Fin (m + 1)) K} {E : MvPowerSeries (Fin 1) K} {d : ℕ} (h : axis F = MvPowerSeries.X 0 ^ d * E) (hE : MvPowerSeries.constantCoeff E ≠ 0) : IsRegularIn F d

If F(x_0, 0) = x_0^d E(x_0) with E(0) ≠ 0, then F is x_0-regular of order d.

Preparation at function level

theorem AnalyticAt.exists_weierstrass_product_nhd {K : Type u_1} [RCLike K] {m : ℕ} {f : (Fin (m + 1) → K) → K} (hf : AnalyticAt K f 0) {d : ℕ} (hd : ∃ (e : K → K), AnalyticAt K e 0 ∧ e 0 ≠ 0 ∧ ∀ᶠ (t : K) in nhds 0, f (Pi.single 0 t) = t ^ d * e t) : ∃ (ρ : Analytic.Radius (m + 1)) (u : (Fin (m + 1) → K) → K) (c : Fin d → (Fin m → K) → K), AnalyticOnNhd K u (Analytic.polydisc K ρ) ∧ (∀ x ∈ Analytic.polydisc K ρ, u x ≠ 0) ∧ (∀ (j : Fin d), AnalyticOnNhd K (c j) (Analytic.polydisc K ⟨fun (k : Fin m) => ↑ρ k.succ, ⋯⟩)) ∧ (∀ (j : Fin d), c j 0 = 0) ∧ ∀ x ∈ Analytic.polydisc K ρ, f x = u x * (x 0 ^ d + ∑ j : Fin d, c j (Fin.tail x) * x 0 ^ (d - 1 - ↑j))

Function-level preparation on a product polydisc: an analytic f near 0 whose restriction to the x_0-axis is t^d times an analytic unit is u · P on a polydisc, with u analytic and nonvanishing there and the coefficients c_j of the Weierstrass polynomial P analytic on the tail polydisc and vanishing at 0 [BM88, proof of Theorem 4.4, p. 24].