Analytic monic normalization across degree drops

For an analytic coefficient family F and a fixed degree d, form the monic polynomial with lower coefficients (F x).coeff i * (F x).coeff d ^ (d - 1 - i). Its coefficients are analytic even where the leading coefficient of F vanishes. At every nonzero degree-d fiber this polynomial is the integral normalization of F x; its roots are scaled by the leading coefficient and its discriminant has the corresponding normalization factor.

This reduces nonmonic analytic polynomial families to monic families without dividing by a possibly vanishing leading coefficient. In particular, when the leading coefficient and the discriminant are powers of a distinguished parameter times analytic units, the normalized discriminant has the same form away from the exceptional hyperplane. A monic root theorem can then be applied to the normalized family and its roots rescaled on the punctured domain.

References

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

theorem TauCeti.exists_analytic_monic_normalization {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {S : Set E} {F : E → Polynomial 𝕜} {d : ℕ} (hF : ∀ i ≤ d, AnalyticOnNhd 𝕜 (fun (x : E) => (F x).coeff i) S) : ∃ (Q : E → Polynomial 𝕜), (∀ (x : E), (Q x).Monic ∧ (Q x).natDegree = d) ∧ (∀ (i : ℕ), AnalyticOnNhd 𝕜 (fun (x : E) => (Q x).coeff i) S) ∧ ∀ (x : E), (F x).natDegree = d → F x ≠ 0 → Q x = (F x).integralNormalization

An analytic coefficient family has an analytic monic normalization of any fixed degree d. It agrees with integral normalization at each nonzero degree-d fiber. The normalized family remains analytic at points where the original degree drops. No openness or finite-dimensionality assumption is needed.