Regularized Weierstrass preparation for holomorphic germs

This module joins the Taylor-line regularization theorem to the pinned classical Weierstrass preparation theorem. It records the coordinate pullback as an equality of raw function germs, so downstream commutative-algebra arguments do not depend on a hidden choice of representative.

theorem LocalComplexGeometry.WPTBridge.representative_not_eventually_zero {n : ℕ} {f : ↥(HolomorphicGerm n)} (hf : f ≠ 0) {F : ComplexEuclidean n → ℂ} (hrep : ↑F = ↑f) : ¬F =ᶠ[nhds 0] fun (x : ComplexEuclidean n) => 0

A representative of a nonzero holomorphic germ is not locally zero.

theorem LocalComplexGeometry.WPTBridge.representative_value_eq_evalAtOrigin {n : ℕ} {f : ↥(HolomorphicGerm n)} {F : ComplexEuclidean n → ℂ} (hrep : ↑F = ↑f) : F 0 = evalAtOrigin f

Evaluation of an analytic representative agrees with evaluation of its germ.

theorem LocalComplexGeometry.WPTBridge.exists_regularized_weierstrassPreparation {n : ℕ} {f : ↥(HolomorphicGerm (n + 1))} (hf_ne : f ≠ 0) : ∃ (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (d : ℕ) (H : ClassicalComplexWPT.Ambient n → ℂ) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (u : ClassicalComplexWPT.Ambient n → ℂ), AnalyticAt ℂ H 0 ∧ (↑fun (x : ComplexEuclidean (n + 1)) => H ((wptAmbientEquiv n) x)) = ↑((coordinatePullback L) f) ∧ H 0 = evalAtOrigin f ∧ ClassicalComplexWPT.ExactOrderInLastVariable H d ∧ ClassicalComplexWPT.IsWeierstrassPreparation H d a u

Regularized preparation of a nonzero holomorphic germ.

H is written in WPT's product coordinates. Composing it with the standard successor-coordinate splitting represents exactly the coordinate pullback of the original germ. The equality H 0 = evalAtOrigin f makes the positive-order corollary independent of representatives.

theorem LocalComplexGeometry.WPTBridge.exists_regularized_weierstrassPreparation_pos {n : ℕ} {f : ↥(HolomorphicGerm (n + 1))} (hf_ne : f ≠ 0) (hf_zero : evalAtOrigin f = 0) : ∃ (L : ComplexEuclidean (n + 1) ≃L[ℂ] ComplexEuclidean (n + 1)) (d : ℕ) (H : ClassicalComplexWPT.Ambient n → ℂ) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (u : ClassicalComplexWPT.Ambient n → ℂ), 0 < d ∧ AnalyticAt ℂ H 0 ∧ (↑fun (x : ComplexEuclidean (n + 1)) => H ((wptAmbientEquiv n) x)) = ↑((coordinatePullback L) f) ∧ H 0 = 0 ∧ ClassicalComplexWPT.ExactOrderInLastVariable H d ∧ ClassicalComplexWPT.IsWeierstrassPreparation H d a u

For a nonzero germ vanishing at the origin, the regularized prepared polynomial has positive degree.