Laurent forms of nonmonic polynomial roots

For a nonmonic polynomial family, multiplying roots by the leading coefficient gives roots of its integral normalization. Suppose these rescaled roots extend analytically across a distinguished hyperplane. If both the leading and constant coefficients are powers of the distinguished variable times analytic units, each original root is a Laurent power times an analytic unit. The exponent is independent of the other parameters, so the possibility of a pole does not vary with them.

The constant coefficient hypothesis is essential: for y * X - x, the rescaled root is x, which has no such unit form near (0, 0). The theorem below extracts the Laurent forms from an already supplied analytic splitting of the normalized family; it does not construct that splitting or the power substitution that produces it. Repeated roots are allowed. The leading coefficient is the coefficient at the fixed punctured-fiber degree; the degree may drop on the hyperplane.

References

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

theorem TauCeti.exists_root_eq_zpow_mul_unit {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {d a c : ℕ} (hd : 0 < d) {P : E × 𝕜 → Polynomial 𝕜} {r s : Fin d → E × 𝕜 → 𝕜} {x₀ : E} {y₀ : 𝕜} {u v : E × 𝕜 → 𝕜} (hs : ∀ (i : Fin d), AnalyticAt 𝕜 (s i) (x₀, y₀)) (hu : AnalyticAt 𝕜 u (x₀, y₀)) (hu0 : u (x₀, y₀) ≠ 0) (hv : AnalyticAt 𝕜 v (x₀, y₀)) (hv0 : v (x₀, y₀) ≠ 0) (hnorm : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → (P p).integralNormalization = ∏ i : Fin d, (Polynomial.X - Polynomial.C (s i p))) (hlead : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (P p).coeff d = (p.2 - y₀) ^ c * v p) (hconst : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (P p).coeff 0 = (p.2 - y₀) ^ a * u p) (hscale : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → ∀ (i : Fin d), (P p).coeff d * r i p = s i p) : ∃ (m : Fin d → ℕ) (w : Fin d → E × 𝕜 → 𝕜), (∀ (i : Fin d), AnalyticAt 𝕜 (w i) (x₀, y₀)) ∧ (∀ (i : Fin d), w i (x₀, y₀) ≠ 0) ∧ ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), (∀ (i : Fin d), w i p ≠ 0) ∧ (p.2 ≠ y₀ → ∀ (i : Fin d), r i p = (p.2 - y₀) ^ (↑(m i) - ↑c) * w i p)

Laurent unit forms of nonmonic roots. Suppose the leading and constant coefficients of a positive-degree family are centered powers times analytic units. Given an analytic extension s of the leading-coefficient multiples of a complete list r of roots, expressed by a splitting of the integral normalization off the hyperplane, each r i is locally (y - y₀) ^ (m i - c) * w i, where m i is natural and w i is an analytic unit.

The exponent c is that of the leading coefficient. The Laurent equality holds off the hyperplane, on one common neighborhood for every label. The units are nonzero on that neighborhood, including on the hyperplane. No analyticity of the original roots at a pole is assumed, and no simplicity assumption is imposed.