Nonmonic Puiseux branches and pole removal

A polynomial family with analytic coefficients, fixed degree and nonzero discriminant on a punctured product splits after a power substitution into distinct analytic linear factors. If its leading coefficient is y ^ a times a nowhere-zero analytic function on the full product, multiplication of every substituted root by t ^ (n * a) gives an analytic extension across t = 0. Degree drops and root collisions on that hyperplane are allowed.

The construction uses integral normalization, whose coefficients remain analytic through a vanishing leading coefficient. Apply the monic punctured splitting theorem to this family, divide its roots by the original leading coefficient off the hyperplane, and apply exists_analyticOnNhd_pow_mul_of_isRoot to extend the scaled branches. The monic construction is exists_analyticOnNhd_eq_prod_X_sub_C_powerSubstitution, and the analytic coefficient normalization is TauCeti.exists_analytic_monic_normalization. No root branches or analytic splitting are assumed. The discriminant need only be nonzero off the hyperplane; in particular it may be a power of the parameter times a unit. No condition on the constant coefficient is needed for construction or pole removal. A condition on that coefficient is needed to extract nonvanishing Laurent units from the extended branches.

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_eq_C_mul_prod_X_sub_C_powerSubstitution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {F : E × ℂ → Polynomial ℂ} {d n : ℕ} {R R' : ℝ} [CompleteSpace E] [SimplyConnectedSpace ↑U] (hU : IsOpen U) (hR' : 0 < R') (hn : n ≠ 0) (hR : R' ^ n ≤ R) (hdvd : d.factorial ∣ n) (hF : ∀ i ≤ d, AnalyticOnNhd ℂ (fun (b : E × ℂ) => (F b).coeff i) (U ×ˢ (Metric.ball 0 R \ {0}))) (hdeg : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).natDegree = d) (hsep : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).Separable) : ∃ (r : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (r i) (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 ^ n) = Polynomial.C ((F (b.1, b.2 ^ n)).coeff d) * ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i b))

A nonmonic analytic family of fixed degree with separable fibers splits on a punctured product after a power substitution divisible by the factorial of its degree. The resulting branches are distinct and give a complete factorization with the original leading coefficient. No behavior at the puncture is assumed or asserted.

theorem TauCeti.Polynomial.exists_analyticOnNhd_nonmonic_powerSubstitution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {F : E × ℂ → Polynomial ℂ} {u : E × ℂ → ℂ} {d n a : ℕ} {R R' : ℝ} [FiniteDimensional ℂ E] [SimplyConnectedSpace ↑U] (hU : IsOpen U) (hR' : 0 < R') (hn : n ≠ 0) (hR : R' ^ n ≤ R) (hdvd : d.factorial ∣ n) (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) (hlc : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).coeff d = b.2 ^ a * u b) : ∃ (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 ^ (n * 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 ^ n) = Polynomial.C ((F (b.1, b.2 ^ n)).coeff d) * ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i b))

Construct nonmonic Puiseux branches with removable poles. Suppose the coefficients of F through degree d are analytic on the full product, its degree is d and its discriminant is nonzero off y = 0, and its degree-d coefficient is y ^ a * u there, with u analytic and nowhere zero on the full product. For any positive power substitution divisible by d!, on a suitably resized disc there are d distinct analytic roots giving a complete factorization. Each t ^ (n * a) * r i extends analytically to the full product. The extended functions may vanish or coincide at t = 0; the original fibers there may have smaller degree or be zero. Degree zero is included.