Continuity of the roots of a polynomial, with multiplicities

Mathlib's Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt shows that each root of a monic polynomial f has a root of every nearby monic polynomial g close to it. That does not control multiplicities: a double root of f could be approximated by a single root of g, the second root of g going elsewhere. This file proves the multiplicity-sensitive statement over a proper algebraically closed normed field, ℂ being the case of interest: the roots of g, counted with multiplicity, can be matched bijectively with those of f so that matched roots are close.

The input is TauCeti.Sym.eventually_exists_ofFn_eq_coeffEquiv_symm, the continuity of the inverse of the elementary symmetric chart TauCeti.Sym.coeffHomeomorph, which comes from Cauchy's bound Polynomial.cauchyBound through properness of the coefficient map. Nothing here chooses a continuous labelling of the roots; the matching is made separately for each nearby polynomial.

Main results

• Polynomial.Monic.exists_prod_X_sub_C_norm_sub_lt: continuity of roots. For monic f and ε > 0 there is δ > 0 such that every monic g of the same degree whose coefficients are δ-close to those of f admits enumerations a, b of the roots of f and g, with multiplicity, satisfying ‖a i - b i‖ < ε.
• Polynomial.Monic.exists_prod_X_sub_C_norm_sub_lt_iff: when the ε-discs around the distinct roots of f are disjoint, such a matching exists exactly when every disc contains as many roots of g as the multiplicity of its centre, and no root of g lies outside the discs.
• Polynomial.Monic.exists_countP_roots_mem_ball_eq_rootMultiplicity: the resulting disc form of continuity of roots.
• Polynomial.eventually_exists_C_mul_prod_X_sub_C_norm_sub_lt: the matching for a family of polynomials of fixed degree with continuous coefficients, normalized by its nonvanishing leading coefficient.
• Polynomial.eventually_exists_bijOn_roots_toFinset: if moreover no nearby member of the family has more distinct roots than the central one, the distinct roots of nearby members correspond bijectively to those of the central one, with matched roots close and of equal multiplicity.

References

• S. Basu, R. Pollack, M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Springer, 2006, §5.1 (continuity of the roots of a polynomial with respect to its coefficients).

theorem Polynomial.Monic.exists_prod_X_sub_C_norm_sub_lt_iff {K : Type u_1} [NormedField K] [IsAlgClosed K] {f g : Polynomial K} (hf : f.Monic) (hg : g.Monic) (hdeg : g.natDegree = f.natDegree) {ε : ℝ} (hsep : ∀ z ∈ f.roots, ∀ w ∈ f.roots, z ≠ w → 2 * ε ≤ ‖z - w‖) : (∃ (a : Fin f.natDegree → K) (b : Fin f.natDegree → K), f = ∏ i : Fin f.natDegree, (X - C (a i)) ∧ g = ∏ i : Fin f.natDegree, (X - C (b i)) ∧ ∀ (i : Fin f.natDegree), ‖a i - b i‖ < ε) ↔ (∀ z ∈ f.roots, Multiset.countP (fun (x : K) => x ∈ Metric.ball z ε) g.roots = rootMultiplicity z f) ∧ ∀ w ∈ g.roots, ∃ z ∈ f.roots, ‖w - z‖ < ε

Matching roots versus counting them in discs. Let f and g be monic of the same degree, and suppose the ε-discs around the distinct roots of f are pairwise disjoint. Then the roots of f and g, with multiplicity, can be enumerated so that matched roots are at distance less than ε exactly when each disc around a root z of f contains rootMultiplicity z f roots of g, counted with multiplicity, and every root of g lies in one of these discs.

theorem Polynomial.Monic.exists_prod_X_sub_C_norm_sub_lt {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {f : Polynomial K} (hf : f.Monic) {ε : ℝ} (hε : 0 < ε) : ∃ δ > 0, ∀ (g : Polynomial K), g.Monic → g.natDegree = f.natDegree → (∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < δ) → ∃ (a : Fin f.natDegree → K) (b : Fin f.natDegree → K), f = ∏ i : Fin f.natDegree, (X - C (a i)) ∧ g = ∏ i : Fin f.natDegree, (X - C (b i)) ∧ ∀ (i : Fin f.natDegree), ‖a i - b i‖ < ε

Continuity of roots, with multiplicities. For a monic polynomial f and ε > 0, every monic polynomial g of the same degree with coefficients close enough to those of f has its roots matched bijectively with those of f, counted with multiplicity: there are enumerations a and b of the roots of f and g with ‖a i - b i‖ < ε for every i. This includes degree zero.

theorem Polynomial.Monic.exists_countP_roots_mem_ball_eq_rootMultiplicity {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {f : Polynomial K} (hf : f.Monic) {ε : ℝ} (hε : 0 < ε) (hsep : ∀ z ∈ f.roots, ∀ w ∈ f.roots, z ≠ w → 2 * ε ≤ ‖z - w‖) : ∃ δ > 0, ∀ (g : Polynomial K), g.Monic → g.natDegree = f.natDegree → (∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < δ) → (∀ z ∈ f.roots, Multiset.countP (fun (x : K) => x ∈ Metric.ball z ε) g.roots = rootMultiplicity z f) ∧ ∀ w ∈ g.roots, ∃ z ∈ f.roots, ‖w - z‖ < ε

Continuity of roots in discs. If the ε-discs around the distinct roots of a monic polynomial f are pairwise disjoint, then every monic polynomial g of the same degree with coefficients close enough to those of f has, counted with multiplicity, exactly rootMultiplicity z f roots in the disc around each root z of f, and no roots outside these discs.

theorem Polynomial.eventually_exists_C_mul_prod_X_sub_C_norm_sub_lt {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial K} {x₀ : B} {d : ℕ} (hF : ∀ i ≤ d, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : B) in nhds x₀, (F x).degree = ↑d) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∃ (a : Fin d → K) (b : Fin d → K), F x₀ = C (F x₀).leadingCoeff * ∏ i : Fin d, (X - C (a i)) ∧ F x = C (F x).leadingCoeff * ∏ i : Fin d, (X - C (b i)) ∧ ∀ (i : Fin d), ‖a i - b i‖ < ε

Continuity of roots in a family. Let F x be polynomials of degree d, near x₀, whose coefficients of index at most d are continuous at x₀. Then for x near x₀ the roots of F x are matched bijectively, with multiplicity, with those of F x₀: there are enumerations a and b of the roots of F x₀ and F x with ‖a i - b i‖ < ε for every i.

theorem Polynomial.eventually_exists_bijOn_roots_toFinset {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {B : Type u_2} [TopologicalSpace B] {F : B → Polynomial K} {x₀ : B} {d : ℕ} (hF : ∀ i ≤ d, ContinuousAt (fun (x : B) => (F x).coeff i) x₀) (hdeg : ∀ᶠ (x : B) in nhds x₀, (F x).degree = ↑d) (hcard : ∀ᶠ (x : B) in nhds x₀, (F x).roots.toFinset.card ≤ (F x₀).roots.toFinset.card) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∃ (e : K → K), Set.BijOn e ↑(F x₀).roots.toFinset ↑(F x).roots.toFinset ∧ ∀ z ∈ (F x₀).roots, ‖e z - z‖ < ε ∧ rootMultiplicity (e z) (F x) = rootMultiplicity z (F x₀)

Distinct roots in a family. Let F x be polynomials of degree d, near x₀, whose coefficients of index at most d are continuous at x₀, and suppose that near x₀ the polynomial F x has at most as many distinct roots as F x₀. Then for x near x₀ there is a bijection e from the distinct roots of F x₀ onto those of F x that moves each root by less than ε and preserves its multiplicity.