Classical complex-analytic Weierstrass preparation

This module assembles the general analytic existence construction and its full germ uniqueness theorem into the exact independently frozen public result.

theorem ClassicalComplexWPT.classicalComplexWeierstrassPreparation (n d : ℕ) (f : Ambient n → ℂ) (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f d) : ∃ (a : Fin d → Base n → ℂ) (u : Ambient n → ℂ), IsWeierstrassPreparation f d a u ∧ ∀ (a' : Fin d → Base n → ℂ) (u' : Ambient n → ℂ), IsWeierstrassPreparation f d a' u' → (∀ (i : Fin d), a i =ᶠ[nhds 0] a' i) ∧ u =ᶠ[nhds 0] u'

Classical complex-analytic Weierstrass preparation at the origin, including existence and uniqueness of every coefficient germ and of the unit germ. The statement includes n = 0 and d = 0.

theorem ClassicalComplexWPT.exists_open_preparation_neighborhood (n d : ℕ) (f : Ambient n → ℂ) (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f d) : ∃ (a : Fin d → Base n → ℂ) (u : Ambient n → ℂ) (s : Set (Ambient n)), IsWeierstrassPreparation f d a u ∧ IsOpen s ∧ 0 ∈ s ∧ (∀ x ∈ s, u x ≠ 0) ∧ ∀ x ∈ s, f x = u x * preparedPolynomial d a x

Explicit-neighborhood form of preparation: the same witnesses factor f pointwise on an open neighborhood of the origin, throughout which the unit is nonzero.