Extending analytic polynomial root branches across a hyperplane

An analytic root branch of a monic polynomial family on U × (s \ {c₀}) extends analytically to U × s when the lower coefficients are continuous there. A complete factorization extends with all factors, so multiplicities are retained. The extension still solves the polynomial equation, including on the hyperplane. For a nonmonic family of fixed degree off the hyperplane, with continuous coefficients and analytic leading coefficient, multiplying a root branch by the leading coefficient gives an analytic extension. In particular, if that coefficient is (z - c₀)^a times a nowhere-zero analytic function, the branch has a Laurent form with pole order at most a.

These results supply the extension step in Puiseux arguments with parameters; they start with single-valued analytic branches on the punctured domain. No simplicity or distinctness of the roots is required at the hyperplane.

The proofs use Mathlib's Polynomial.integralNormalization to scale a root by the leading coefficient, Cauchy's root bound in coefficient coordinates, and TauCeti.exists_analyticOnNhd_prod_eqOn for joint analytic extension.

Reference: S. McCallum, A. Parusiński, L. Paunescu, Validity proof of Lazard's method for CAD construction, J. Symbolic Comput. 92 (2019), §4.

theorem TauCeti.Polynomial.exists_analyticOnNhd_isRoot_monicOfCoeff {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {s : Set ℂ} {c₀ : ℂ} {d : ℕ} (c : V × ℂ → Fin d → ℂ) {r : V × ℂ → ℂ} (hU : IsOpen U) (hs : IsOpen s) (hc : ContinuousOn c (U ×ˢ s)) (hr : AnalyticOnNhd ℂ r (U ×ˢ (s \ {c₀}))) (hroot : ∀ x ∈ U ×ˢ (s \ {c₀}), (monicOfCoeff (c x)).IsRoot (r x)) : ∃ (g : V × ℂ → ℂ), AnalyticOnNhd ℂ g (U ×ˢ s) ∧ Set.EqOn g r (U ×ˢ (s \ {c₀})) ∧ ∀ x ∈ U ×ˢ s, (monicOfCoeff (c x)).IsRoot (g x)

An analytic root branch of a monic family extends across z = c₀, and its extension remains a root. The coefficients need only be continuous on the full domain. The extension is unique there by TauCeti.eqOn_prod_of_eqOn_prod_diff_singleton.

theorem TauCeti.Polynomial.exists_analyticOnNhd_monicOfCoeff_eq_prod_X_sub_C {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {s : Set ℂ} {c₀ : ℂ} {d : ℕ} (c : V × ℂ → Fin d → ℂ) (r : Fin d → V × ℂ → ℂ) (hU : IsOpen U) (hs : IsOpen s) (hc : ContinuousOn c (U ×ˢ s)) (hr : ∀ (i : Fin d), AnalyticOnNhd ℂ (r i) (U ×ˢ (s \ {c₀}))) (hfac : ∀ x ∈ U ×ˢ (s \ {c₀}), monicOfCoeff (c x) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (r i x))) : ∃ (g : Fin d → V × ℂ → ℂ), (∀ (i : Fin d), AnalyticOnNhd ℂ (g i) (U ×ˢ s) ∧ Set.EqOn (g i) (r i) (U ×ˢ (s \ {c₀}))) ∧ ∀ x ∈ U ×ˢ s, monicOfCoeff (c x) = ∏ i : Fin d, (Polynomial.X - Polynomial.C (g i x))

A complete analytic factorization of a monic family on the punctured domain extends to a factorization on the full domain, even when roots collide at z = c₀. The indexing retains all factors, including repetitions.

theorem TauCeti.Polynomial.exists_analyticOnNhd_coeff_mul_of_isRoot {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {s : Set ℂ} {c₀ : ℂ} {d : ℕ} (F : V × ℂ → Polynomial ℂ) {r : V × ℂ → ℂ} (hU : IsOpen U) (hs : IsOpen s) (hF : ∀ i ≤ d, ContinuousOn (fun (x : V × ℂ) => (F x).coeff i) (U ×ˢ s)) (hl : AnalyticOnNhd ℂ (fun (x : V × ℂ) => (F x).coeff d) (U ×ˢ (s \ {c₀}))) (hd : ∀ x ∈ U ×ˢ (s \ {c₀}), (F x).natDegree = d) (hne : ∀ x ∈ U ×ˢ (s \ {c₀}), F x ≠ 0) (hr : AnalyticOnNhd ℂ r (U ×ˢ (s \ {c₀}))) (hroot : ∀ x ∈ U ×ˢ (s \ {c₀}), (F x).IsRoot (r x)) : ∃ (g : V × ℂ → ℂ), AnalyticOnNhd ℂ g (U ×ˢ s) ∧ Set.EqOn g (fun (x : V × ℂ) => (F x).coeff d * r x) (U ×ˢ (s \ {c₀}))

For a polynomial family with continuous coefficients and fixed degree off z = c₀, multiplying an analytic root branch by the degree-d coefficient removes its singularity. That coefficient may vanish on the hyperplane.

theorem TauCeti.Polynomial.exists_analyticOnNhd_pow_mul_of_isRoot {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℂ V] [FiniteDimensional ℂ V] {U : Set V} {s : Set ℂ} {c₀ : ℂ} {d : ℕ} (F : V × ℂ → Polynomial ℂ) {r u : V × ℂ → ℂ} {a : ℕ} (hU : IsOpen U) (hs : IsOpen s) (hF : ∀ i ≤ d, ContinuousOn (fun (x : V × ℂ) => (F x).coeff i) (U ×ˢ s)) (hd : ∀ x ∈ U ×ˢ (s \ {c₀}), (F x).natDegree = d) (hu : AnalyticOnNhd ℂ u (U ×ˢ s)) (hu0 : ∀ x ∈ U ×ˢ s, u x ≠ 0) (hlc : ∀ x ∈ U ×ˢ (s \ {c₀}), (F x).coeff d = (x.2 - c₀) ^ a * u x) (hr : AnalyticOnNhd ℂ r (U ×ˢ (s \ {c₀}))) (hroot : ∀ x ∈ U ×ˢ (s \ {c₀}), (F x).IsRoot (r x)) : ∃ (g : V × ℂ → ℂ), AnalyticOnNhd ℂ g (U ×ˢ s) ∧ Set.EqOn g (fun (x : V × ℂ) => (x.2 - c₀) ^ a * r x) (U ×ˢ (s \ {c₀}))

If the leading coefficient is (z - c₀)^a times a nowhere-zero analytic function, an analytic root branch has a Laurent form with pole order at most a: (z - c₀)^a * r extends analytically to the full domain.