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.

theorem TauCeti.Polynomial.exists_analyticOnNhd_integralNormalization_eq_prod_X_sub_C_powerSubstitution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set E} {F : E × ℂ → Polynomial ℂ} {u : E × ℂ → ℂ} {d n a : ℕ} {R R' : ℝ} {r g : Fin d → E × ℂ → ℂ} (hn : n ≠ 0) (hR : R' ^ n ≤ R) (hdeg : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).natDegree = d) (hu : AnalyticOnNhd ℂ u (U ×ˢ Metric.ball 0 R)) (hu0 : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), u b ≠ 0) (hlead : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).coeff d = b.2 ^ a * u b) (hg : ∀ (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}))) (hr : ∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), 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))) : ∃ (s : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (s i) (U ×ˢ Metric.ball 0 R')) ∧ (∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), ∀ (i : Fin d), (F (b.1, b.2 ^ n)).coeff d * r i b = s i b) ∧ ∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), (F (b.1, b.2 ^ n)).integralNormalization = ∏ i : Fin d, (Polynomial.X - Polynomial.C (s i b))

Multiplying pole-removed branches of a nonmonic power-substituted splitting by the leading-coefficient unit gives analytic functions on the full product and a complete splitting of integral normalization off the hyperplane, with the same labels. No degree condition on the central fibers, distinctness of the branches, or analyticity of the original branches is required.