Analytic roots after a power substitution

A monic polynomial family of degree d with analytic coefficients and simple roots on U × (ball 0 R \ {0}) admits single-valued analytic root functions after the substitution (w, t) ↦ (w, t ^ n), provided d ! ∣ n and the substituted disc fits inside the original disc. Here U is open and simply connected. The root functions are pointwise distinct and give a complete linear factorization. The degree-zero case gives the empty factorization.

The continuous and analytic splitting theorems give the single-valued root functions needed for Puiseux factorization with parameters. These functions are defined on the punctured domain only; extension across the missing hyperplane requires a separate removable-singularity argument.

References

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

theorem TauCeti.Polynomial.exists_continuousMap_prod_X_sub_C_powerSubstitution {U : Type u_1} [TopologicalSpace U] [SimplyConnectedSpace U] [LocallyPathConnectedSpace U] {d n : ℕ} {R R' : ℝ} {F : U × ↑(Metric.ball 0 R \ {0}) → Polynomial ℂ} (hF : ∀ i ≤ d, Continuous fun (b : U × ↑(Metric.ball 0 R \ {0})) => (F b).coeff i) (hmonic : ∀ (b : U × ↑(Metric.ball 0 R \ {0})), (F b).Monic) (hdeg : ∀ (b : U × ↑(Metric.ball 0 R \ {0})), (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 → C(U × ↑(Metric.ball 0 R' \ {0}), ℂ)), ∀ (b : U × ↑(Metric.ball 0 R' \ {0})), (Function.Injective fun (i : Fin d) => (r i) b) ∧ F ((powerSubstitution U hn hR) b) = ∏ i : Fin d, (Polynomial.X - Polynomial.C ((r i) b))

A continuous monic family of degree d, separable over a punctured disc, splits into d pointwise distinct continuous linear factors after a power substitution of exponent divisible by d !. The parameter space can be any simply connected, locally path connected space.

theorem TauCeti.Polynomial.exists_analyticOnNhd_prod_X_sub_C_powerSubstitution {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {U : Set E} (hU : IsOpen U) [SimplyConnectedSpace ↑U] {F : E × ℂ → Polynomial ℂ} {d n : ℕ} {R R' : ℝ} (hF : ∀ i ≤ d, AnalyticOnNhd ℂ (fun (b : E × ℂ) => (F b).coeff i) (U ×ˢ (Metric.ball 0 R \ {0}))) (hmonic : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (F b).Monic) (hdeg : ∀ b ∈ U ×ˢ (Metric.ball 0 R \ {0}), (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' \ {0}))) ∧ ∀ b ∈ U ×ˢ (Metric.ball 0 R' \ {0}), (Function.Injective fun (i : Fin d) => r i b) ∧ F (b.1, b.2 ^ n) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i b))

A monic family with analytic coefficients and simple roots on an open simply connected parameter domain times a punctured disc splits into pointwise distinct analytic linear factors there after t ↦ t ^ n, for any nonzero n divisible by d !. The functions in the conclusion are ambient functions, analytic on the punctured product; nothing is asserted at t = 0.