Differences of analytic polynomial roots

Suppose a polynomial family splits locally into analytic linear factors and its discriminant is a power of one distinguished variable times an analytic unit. Every difference of two distinctly labelled roots is then a power of that variable times an analytic unit as well. Roots may coincide on the distinguished hyperplane; their differences have constant finite order along it.

The discriminant identity used here is Polynomial.discr_prod_X_sub_C. Each root difference occurs twice in that product. The analytic factor-order theorem extracts its power-times-unit form without assuming that its slice order is already constant.

References

• S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4.

theorem TauCeti.exists_root_sub_eq_pow_mul_unit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {r : Fin n → E × 𝕜 → 𝕜} {P : E × 𝕜 → Polynomial 𝕜} {x₀ : E} {y₀ : 𝕜} (hr : ∀ (i : Fin n), AnalyticAt 𝕜 (r i) (x₀, y₀)) (hP : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), P p = ∏ i : Fin n, (Polynomial.X - Polynomial.C (r i p))) {a : ℕ} {u : E × 𝕜 → 𝕜} (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hdiscr : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (P p).discr = (p.2 - y₀) ^ a * u p) {i j : Fin n} (hij : i ≠ j) : ∃ (b : ℕ) (v : E × 𝕜 → 𝕜), AnalyticAt 𝕜 v (x₀, y₀) ∧ v (x₀, y₀) ≠ 0 ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), r i p - r j p = (p.2 - y₀) ^ b * v p

For an analytic splitting whose discriminant is a centered power times an analytic unit, every difference of roots with distinct labels is locally a centered power times an analytic unit. The roots need not be distinct on the distinguished hyperplane.