Monic Puiseux factorization with parameters

A monic polynomial family with analytic coefficients on U × ball 0 R, whose discriminant is y ^ a * u with u nowhere zero, splits into analytic linear factors after y = t ^ d!. The factorization holds on the full substituted disc, including t = 0, where roots may collide. The parameter domain U can be any open simply connected subset of a finite dimensional complex normed space, in particular a polydisc.

exists_analyticOnNhd_prod_X_sub_C_powerSubstitution_ball gives the full-disc splitting under the weaker assumption of separability off the hyperplane, for any nonzero multiple of d! and any substituted radius that fits. The discriminant form of the result is exists_analyticOnNhd_prod_X_sub_C_of_discr_eq_pow_mul; it chooses a positive substituted radius and also gives the local power-times-unit form of every difference of distinct root labels at each point of the hyperplane. The degree-zero case is included.

The splitting uses the punctured root covering and monodromy theorem exists_analyticOnNhd_eq_prod_X_sub_C_powerSubstitution, followed by the joint analytic extension exists_analyticOnNhd_monicOfCoeff_eq_prod_X_sub_C. The root-difference conclusion uses TauCeti.exists_root_sub_eq_pow_mul_unit.

References

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

theorem TauCeti.Polynomial.exists_analyticOnNhd_prod_X_sub_C_powerSubstitution_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] {U : Set E} [SimplyConnectedSpace ↑U] {F : E × ℂ → Polynomial ℂ} {d n : ℕ} {R R' : ℝ} (hU : IsOpen U) (hR' : 0 < R') (hF : ∀ i < d, AnalyticOnNhd ℂ (fun (b : E × ℂ) => (F b).coeff i) (U ×ˢ (Metric.ball 0 R \ {0}))) (hcoeff : ∀ i < d, ContinuousOn (fun (b : E × ℂ) => (F b).coeff i) (U ×ˢ Metric.ball 0 R)) (hmonic : ∀ b ∈ U ×ˢ Metric.ball 0 R, (F b).Monic) (hdeg : ∀ b ∈ U ×ˢ Metric.ball 0 R, (F b).natDegree = d) (hsep : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).Separable) (hn : n ≠ 0) (hR : R' ^ n ≤ R) (hdvd : d.factorial ∣ n) : ∃ (r : Fin d → E × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (r i) (U ×ˢ Metric.ball 0 R')) ∧ (∀ b ∈ U ×ˢ Metric.ball 0 R', F (b.1, b.2 ^ n) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i b))) ∧ ∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), Function.Injective fun (i : Fin d) => r i b

A monic family with continuous coefficients, analytic and separable off y = 0, splits after a power substitution into analytic linear factors on the full disc. The factors retain their multiplicities at t = 0 and are pointwise distinct off that hyperplane. The exponent can be any nonzero multiple of d!.

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

Monic Puiseux with parameters. If the discriminant is y ^ a * u, with analytic nowhere-zero u, substitution by t ^ d! gives an analytic splitting on a full disc of positive radius. At every parameter on t = 0, every difference of distinct root labels is locally a power of t times an analytic unit. The branches may collide at t = 0, but are pointwise distinct elsewhere.