Real descent of finite root labellings

A finite continuous complete labelling of the complex roots of a real polynomial family with persistent collisions descends to the labels real at the central parameter. Analyticity of their real parts gives analytic real sections. A complete root multiset and a locally constant collision relation also give constant multiplicities; removing repeated labels then yields strictly ordered sections on one common open neighborhood.

These results allow repeated labels and empty root families. They require neither monicity nor continuity of the polynomial coefficients, and apply to arbitrary real normed parameter spaces. Preparation of the complex labels and their collision relation is separate.

References

S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, Journal of Symbolic Computation 92 (2019), 52–69, Section 4.

theorem TauCeti.exists_analyticAt_real_roots_of_persistent_collisions {B : Type u_1} {ι : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] {F : B → Polynomial ℝ} {r : ι → B → ℂ} {b₀ : B} [Finite ι] (hr : ∀ (i : ι), ContinuousAt (r i) b₀) (hre : ∀ (i : ι), AnalyticAt ℝ (fun (b : B) => (r i b).re) b₀) (hroot : ∀ᶠ (b : B) in nhds b₀, ∀ (z : ℂ), (Polynomial.map (algebraMap ℝ ℂ) (F b)).IsRoot z ↔ ∃ (i : ι), r i b = z) (hcollision : ∀ (i j : ι), r j b₀ = r i b₀ → r j =ᶠ[nhds b₀] r i) : ∃ (s : { i : ι // (r i b₀).im = 0 } → B → ℝ), (∀ (i : { i : ι // (r i b₀).im = 0 }), AnalyticAt ℝ (s i) b₀) ∧ ∀ᶠ (b : B) in nhds b₀, (∀ (i : { i : ι // (r i b₀).im = 0 }), ↑(s i b) = r (↑i) b) ∧ ∀ (z : ℝ), (F b).IsRoot z ↔ ∃ (i : { i : ι // (r i b₀).im = 0 }), s i b = z

Descend a finite continuous complete complex root labelling with persistent central collisions to analytic real sections, retaining repeated labels. Only the real parts need be analytic; the selected sections agree with their complex labels near the center.

theorem TauCeti.exists_analyticOnNhd_ordered_real_roots_of_persistent_collisions {B : Type u_1} {ι : Type u_2} [NormedAddCommGroup B] [NormedSpace ℝ B] {F : B → Polynomial ℝ} {r : ι → B → ℂ} {b₀ : B} [Fintype ι] (hr : ∀ (i : ι), ContinuousAt (r i) b₀) (hre : ∀ (i : ι), AnalyticAt ℝ (fun (b : B) => (r i b).re) b₀) (hroots : ∀ᶠ (b : B) in nhds b₀, (Polynomial.map (algebraMap ℝ ℂ) (F b)).roots = Multiset.map (fun (i : ι) => r i b) Finset.univ.val) (hF : ∀ᶠ (b : B) in nhds b₀, F b ≠ 0) (hcollision : ∀ᶠ (b : B) in nhds b₀, ∀ (i j : ι), r i b = r j b ↔ r i b₀ = r j b₀) : ∃ (k : ℕ) (s : Fin k → B → ℝ) (U : Set B), IsOpen U ∧ b₀ ∈ U ∧ (∀ b ∈ U, F b ≠ 0) ∧ (∀ (i : Fin k), AnalyticOnNhd ℝ (s i) U) ∧ (∀ b ∈ U, StrictMono fun (i : Fin k) => s i b) ∧ (∀ b ∈ U, ∀ (z : ℝ), (F b).IsRoot z ↔ ∃ (i : Fin k), s i b = z) ∧ (∀ (i : Fin k), 0 < Polynomial.rootMultiplicity (s i b₀) (F b₀)) ∧ ∀ b ∈ U, ∀ (i : Fin k), Polynomial.rootMultiplicity (s i b) (F b) = Polynomial.rootMultiplicity (s i b₀) (F b₀)

A finite complete root multiset with locally constant collisions gives strictly ordered analytic real root sections with constant positive multiplicities. The real parts of the continuous labels need be analytic only at the central parameter. Nonzeroness is retained on the resulting neighborhood, including when there are no real roots.