Analytic roots on analytic submanifolds

Continuous root functions of polynomial families with intrinsically analytic coefficients and locally constant positive multiplicity are intrinsically analytic on an analytic submanifold. Degree bounds are needed only on the submanifold, locally at each point; the ambient fibers can behave differently. Apply the constant-multiplicity root theorem in the free coordinates of a chart.

This is the regularity step turning continuous delineations into analytic delineations.

References

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

theorem TauCeti.IsAnalyticSubmanifold.analyticOnSubmanifold_of_rootMultiplicity_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CharZero 𝕜] [CompleteSpace 𝕜] {n d : ℕ} {S : Set (Fin n → 𝕜)} {F : (Fin n → 𝕜) → Polynomial 𝕜} {r : (Fin n → 𝕜) → 𝕜} (hS : IsAnalyticSubmanifold d S) (hF : ∀ (i : ℕ), AnalyticOnSubmanifold d (fun (x : Fin n → 𝕜) => (F x).coeff i) S) (hdeg : ∀ x ∈ S, ∃ (b : ℕ), ∀ᶠ (y : Fin n → 𝕜) in nhdsWithin x S, (F y).natDegree ≤ b) (hr : ContinuousOn r S) (hmult : ∀ x ∈ S, ∃ (m : ℕ), 0 < m ∧ ∀ᶠ (y : Fin n → 𝕜) in nhdsWithin x S, Polynomial.rootMultiplicity (r y) (F y) = m) : AnalyticOnSubmanifold d r S

A continuous root function on an analytic submanifold is intrinsically analytic if the coefficients are intrinsically analytic and its positive multiplicity is locally constant. Only local bounds on the degrees of fibers over the submanifold are required.