Analytic roots with constant multiplicity

A continuous root of an analytic polynomial family is analytic if its positive multiplicity is locally constant. This includes repeated roots: the derivative of order one less than that multiplicity has a simple root, to which the analytic implicit-root theorem applies.

This supplies the analytic regularity of continuous root sections when delineability has already established constant multiplicities. The polynomial degree need only be locally bounded; no separability of the original family is required.

References

S. McCallum, An improved projection operation for cylindrical algebraic decomposition, Springer (1998), 242–268 (analytic delineability).

theorem TauCeti.Polynomial.analyticAt_of_eventually_rootMultiplicity_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {F : E → Polynomial 𝕜} {r : E → 𝕜} {x₀ : E} {d m : ℕ} (hF : ∀ i ≤ d, AnalyticAt 𝕜 (fun (x : E) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : E) in nhds x₀, (F x).natDegree ≤ d) (hr : ContinuousAt r x₀) (hm : 0 < m) (hmult : ∀ᶠ (x : E) in nhds x₀, Polynomial.rootMultiplicity (r x) (F x) = m) : AnalyticAt 𝕜 r x₀

A continuous root of an analytic polynomial family is analytic wherever its positive multiplicity is locally constant. The degrees of the fibers need only be locally bounded.