Continuous monic gcds of polynomial families

The monic gcd of two polynomial families has continuous coefficients wherever the degrees of both inputs and of their gcd are locally constant. At a strict gcd index it is the subresultant polynomial divided by its nonzero principal coefficient. At a terminal index it is the monic normalization of the input of smaller degree. The terminal cases include nonzero constants and one input dividing the other.

Consequently, every common root at a parameter is approximated by common roots at nearby parameters. This supplies the common-root persistence needed to make individual root matchings agree for several polynomials; fixed input degrees alone do not ensure persistence.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 4 and 5 (subresultant gcd recovery and continuity of roots).

theorem TauCeti.continuousAt_subresultantCoeff {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {F G : B → Polynomial R} {x₀ : B} {m n : ℕ} (hF : ∀ i ≤ m, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hG : ∀ i ≤ n, ContinuousAt (fun (x : B) => (G x).coeff i) x₀) (j k : ℕ) : ContinuousAt (fun (x : B) => (F x).subresultantCoeff (G x) m n j k) x₀

A fixed-bound subresultant coefficient minor depends continuously on the input coefficients. Only coefficients up to the respective formal bounds need be continuous.

theorem TauCeti.continuousAt_coeff_subresultant {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] {F G : B → Polynomial R} {x₀ : B} {m n : ℕ} (hF : ∀ i ≤ m, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hG : ∀ i ≤ n, ContinuousAt (fun (x : B) => (G x).coeff i) x₀) (j k : ℕ) : ContinuousAt (fun (x : B) => ((F x).subresultant (G x) m n j).coeff k) x₀

Every coefficient of a fixed-bound subresultant polynomial is continuous in the input coefficients, including outside the strict-index range where the polynomial is zero.

theorem TauCeti.continuousAt_coeff_normalize {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [Field R] [DecidableEq R] [TopologicalSpace R] [IsTopologicalDivisionRing R] {F : B → Polynomial R} {x₀ : B} {m : ℕ} (hF : ∀ i ≤ m, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : B) in nhds x₀, (F x).degree = ↑m) (k : ℕ) : ContinuousAt (fun (x : B) => (normalize (F x)).coeff k) x₀

Monic normalization has continuous coefficients on a family of fixed finite degree.

theorem TauCeti.continuousAt_coeff_normalize_gcd {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [Field R] [DecidableEq R] [TopologicalSpace R] [IsTopologicalDivisionRing R] {F G : B → Polynomial R} {x₀ : B} {m n j : ℕ} (hF : ∀ i ≤ m, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hG : ∀ i ≤ n, ContinuousAt (fun (x : B) => (G x).coeff i) x₀) (hdegF : ∀ᶠ (x : B) in nhds x₀, (F x).degree = ↑m) (hdegG : ∀ᶠ (x : B) in nhds x₀, (G x).degree = ↑n) (hgcd : ∀ᶠ (x : B) in nhds x₀, (EuclideanDomain.gcd (F x) (G x)).natDegree = j) (k : ℕ) : ContinuousAt (fun (x : B) => (normalize (EuclideanDomain.gcd (F x) (G x))).coeff k) x₀

The monic gcd has continuous coefficients when both input degrees and the gcd degree are locally constant. The gcd may have the full degree of either input; neither input need be monic or squarefree. Finite input degrees exclude zero polynomials.

theorem TauCeti.eventually_exists_common_root_norm_sub_lt {B : Type u_1} {R : Type u_2} [TopologicalSpace B] [NormedField R] [DecidableEq R] [IsAlgClosed R] [ProperSpace R] {F G : B → Polynomial R} {x₀ : B} {m n j : ℕ} (hF : ∀ i ≤ m, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hG : ∀ i ≤ n, ContinuousAt (fun (x : B) => (G x).coeff i) x₀) (hdegF : ∀ᶠ (x : B) in nhds x₀, (F x).degree = ↑m) (hdegG : ∀ᶠ (x : B) in nhds x₀, (G x).degree = ↑n) (hgcd : ∀ᶠ (x : B) in nhds x₀, (EuclideanDomain.gcd (F x) (G x)).natDegree = j) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∀ (z : R), (F x₀).IsRoot z → (G x₀).IsRoot z → ∃ (w : R), (F x).IsRoot w ∧ (G x).IsRoot w ∧ ‖w - z‖ < ε

Common roots persist under continuous variation with locally constant input and gcd degrees: every central common root has a common root arbitrarily close in every sufficiently nearby fiber. This does not assume constancy of the number of distinct roots of either input.