Analytic root branches after a power substitution

A separable polynomial family of constant degree on a product of a simply connected parameter space and a punctured complex disc has finite root monodromy. A power substitution whose exponent is divisible by the factorial of the degree kills that monodromy. The resulting continuous root branches are analytic when the coefficients are analytic, since all roots on the punctured disc are simple.

TauCeti.Polynomial.exists_analyticOnNhd_eq_prod_X_sub_C_powerSubstitution gives a complete factorization of a monic family into pairwise distinct analytic linear factors after substitution. The functions are defined on the ambient normed space and are analytic on the punctured product; no analyticity at the puncture is asserted. This is the input to removable-singularity arguments that extend the factorization to the full disc, where roots may collide.

The parameter domain may be any open simply connected subset of a complex Banach space, including a polydisc. The substituted disc has radius R', with R' ^ n ≤ R; the exponent may be any nonzero multiple of d!, in particular d! itself. Degree-zero monic families are included.

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_analyticOnNhd_eq_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}))) (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) : ∃ (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 power substitution splits a monic analytic family on a punctured disc. On an open simply connected parameter domain, let F be monic of constant degree d, with analytic coefficients and separable fibres on the punctured product of radius R. For every nonzero multiple n of d! and positive R' with R' ^ n ≤ R, there are d analytic branches on the punctured product of radius R'. They are pointwise distinct and their linear factors multiply to F (x, t ^ n).

The branches are ambient functions, so they can be passed directly to analytic extension results. Their values outside the punctured product are unconstrained. No regularity at t = 0 is required of the original family or asserted of the branches.