Uniform locality of prepared roots

The roots of a positive-degree prepared polynomial converge uniformly to the distinguished point as the base tends to the origin. This is the locality bridge which allows ambient germ identities to be applied simultaneously to every root of a nearby specialized fiber.

theorem LocalComplexGeometry.eventually_appendLast_mem_of_preparedValue_eq_zero {n d : ℕ} (hd : 0 < d) (a : Fin d → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) {V : Set (ComplexEuclidean (n + 1))} (hV : V ∈ nhds 0) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, ∀ (w : ℂ), preparedValue a z w = 0 → (appendLastCLE n) (z, w) ∈ V

Every root of a nearby prepared fiber lies in any prescribed neighborhood of the ambient origin.

theorem LocalComplexGeometry.eventually_on_all_prepared_roots {n d : ℕ} (hd : 0 < d) (a : Fin d → ComplexEuclidean n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) {R : ComplexEuclidean (n + 1) → Prop} (hR : ∀ᶠ (x : ComplexEuclidean (n + 1)) in nhds 0, R x) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, ∀ (w : ℂ), preparedValue a z w = 0 → R ((appendLastCLE n) (z, w))

Predicate form of eventually_appendLast_mem_of_preparedValue_eq_zero: an ambient property which holds near the origin holds simultaneously at all roots of every sufficiently nearby prepared fiber.