Representatives of canonical Weierstrass division

The germ-level division identity becomes one pointwise identity on a common ambient neighborhood after choosing analytic representatives. Uniform prepared-root locality then specializes it simultaneously at every root of a nearby prepared fiber.

theorem LocalComplexGeometry.eventually_representative_preparedGermDivision {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : ∀ᶠ (x : ComplexEuclidean (n + 1)) in nhds 0, HolomorphicGerm.representative h x = HolomorphicGerm.representative (WPTBridge.preparedGermDivisionQuotient a ha ha0 h) x * preparedValue a ((dropLastCLM n) x) ((lastCoordinateCLM n) x) + ∑ i : Fin d, HolomorphicGerm.representative (WPTBridge.preparedGermDivisionRemainder a ha ha0 h i) ((dropLastCLM n) x) * (lastCoordinateCLM n) x ^ ↑i

Chosen representatives satisfy the canonical Weierstrass division identity on one ambient neighborhood.

theorem LocalComplexGeometry.eventually_representative_eq_remainder_on_preparedRoots {n d : ℕ} (hd : 0 < d) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (h : ↥(HolomorphicGerm (n + 1))) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, ∀ (w : ℂ), preparedValue a z w = 0 → HolomorphicGerm.representative h ((appendLastCLE n) (z, w)) = ∑ i : Fin d, HolomorphicGerm.representative (WPTBridge.preparedGermDivisionRemainder a ha ha0 h i) z * w ^ ↑i

At every root of every sufficiently nearby prepared fiber, the chosen representative of a germ equals the specialized polynomial represented by its canonical WPT remainder.