Construction of nonmonic Puiseux Laurent factorizations

A polynomial family with analytic coefficients and nonzero discriminant off a distinguished hyperplane splits after substitution by the factorial of its degree. When its leading and constant coefficients are powers of the distinguished coordinate times analytic units, the roots have Laurent power times unit forms on the whole parameter product. Both the integer exponents and the analytic units are global throughout the simply connected base, and their pole orders are bounded by the substituted leading-coefficient exponent. Degree drops and nullified fibers on the hyperplane are allowed.

The construction joins exists_analyticOnNhd_nonmonic_powerSubstitution, which constructs roots and removes their poles, with TauCeti.exists_root_eq_zpow_mul_unit, which extracts unit forms from the analytic roots of integral normalization. Neither a root labelling nor a splitting is an input. The trailing-coefficient hypothesis prevents roots from vanishing identically or acquiring a parameter-dependent order.

References

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

theorem TauCeti.Polynomial.exists_analyticOnNhd_nonmonic_laurent {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} [SimplyConnectedSpace ↑U] {F : E × ℂ → Polynomial ℂ} {d a c : ℕ} {R : ℝ} {u v : E × ℂ → ℂ} (hU : IsOpen U) (hR : 0 < R) (hF : ∀ i ≤ d, AnalyticOnNhd ℂ (fun (b : E × ℂ) => (F b).coeff i) (U ×ˢ Metric.ball 0 R)) (hdeg : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).natDegree = d) (hdiscr : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).discr ≠ 0) (hu : AnalyticOnNhd ℂ u (U ×ˢ Metric.ball 0 R)) (hu0 : ∀ b ∈ U ×ˢ Metric.ball 0 R, u b ≠ 0) (hv : AnalyticOnNhd ℂ v (U ×ˢ Metric.ball 0 R)) (hv0 : ∀ b ∈ U ×ˢ Metric.ball 0 R, v b ≠ 0) (hlead : ∀ b ∈ U ×ˢ Metric.ball 0 R, (F b).coeff d = b.2 ^ a * u b) (hconst : ∀ b ∈ U ×ˢ Metric.ball 0 R, (F b).coeff 0 = b.2 ^ c * v b) : ∃ (R' : ℝ), 0 < R' ∧ R' ^ d.factorial ≤ R ∧ ∃ (r : Fin d → E × ℂ → ℂ) (g : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (r i) (U ×ˢ (Metric.ball 0 R' \ {0}))) ∧ (∀ (i : Fin d), AnalyticOnNhd ℂ (g i) (U ×ˢ Metric.ball 0 R') ∧ Set.EqOn (g i) (fun (b : E × ℂ) => b.2 ^ (d.factorial * a) * r i b) (U ×ˢ (Metric.ball 0 R' \ {0}))) ∧ (∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), (Function.Injective fun (i : Fin d) => r i b) ∧ F (b.1, b.2 ^ d.factorial) = Polynomial.C ((F (b.1, b.2 ^ d.factorial)).coeff d) * ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i b))) ∧ ∃ (e : Fin d → ℤ) (w : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), -(↑d.factorial * ↑a) ≤ e i) ∧ (∀ (i : Fin d), AnalyticOnNhd ℂ (w i) (U ×ˢ Metric.ball 0 R')) ∧ (∀ (i : Fin d), ∀ b ∈ U ×ˢ Metric.ball 0 R', w i b ≠ 0) ∧ ∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), ∀ (i : Fin d), r i b = b.2 ^ e i * w i b

Nonmonic Puiseux Laurent factorization with parameters. Analytic coefficients, constant degree and nonzero discriminant off y = 0, and power-times-unit leading and constant coefficients suffice to construct a complete distinct splitting after y = t ^ d!. All roots simultaneously have the form t ^ e * w throughout the punctured product, with one integer exponent vector e ≥ -(d! * a) and one analytic nowhere-zero unit per label on the entire product, including t = 0. The same root labels have analytic extensions after multiplication by t ^ (d! * a). The original fibers on the hyperplane may drop degree or be zero. Degree zero is included.