Real roots of a family of real polynomials

Let F x be real polynomials of fixed degree whose coefficients depend continuously on a parameter x. Nearby members of the family can lose real roots, or gain them, when two real roots collide and leave the real line as a pair of complex conjugates, or when such a pair lands on the real line. Both events lower the number of distinct complex roots at the collision. This file shows that if the number of distinct complex roots of F x does not exceed that of F x₀ for x near x₀, then the distinct real roots of F x correspond bijectively to those of F x₀, each moved by an arbitrarily small amount and with its multiplicity unchanged. In particular the number of distinct real roots is then locally constant.

The proof applies Polynomial.eventually_exists_bijOn_roots_toFinset to the complex roots and uses complex conjugation. The disc around a real root of F x₀ contains a single distinct root of F x, and the conjugate of that root is a root in the same disc, so it is real. The discs around the non-real roots of F x₀ are chosen to miss the real line, so they contain no real roots.

Main results

• Polynomial.eventually_exists_bijOn_roots_toFinset_of_card_aroots_le: the distinct real roots of F x and F x₀ correspond bijectively, nearby and with the same multiplicities.
• Polynomial.eventually_card_roots_toFinset_eq_of_card_aroots_le: the number of distinct real roots is locally constant.

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.eventually_exists_bijOn_roots_toFinset_of_card_aroots_le {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {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).aroots ℂ).toFinset.card ≤ ((F x₀).aroots ℂ).toFinset.card) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∃ (e : ℝ → ℝ), Set.BijOn e ↑(F x₀).roots.toFinset ↑(F x).roots.toFinset ∧ ∀ t ∈ (F x₀).roots, |e t - t| < ε ∧ rootMultiplicity (e t) (F x) = rootMultiplicity t (F x₀)

Real roots in a family. Let F x be real 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 complex roots as F x₀. Then for x near x₀ there is a bijection e from the distinct real roots of F x₀ onto those of F x that moves each root by less than ε and preserves its multiplicity.

theorem Polynomial.eventually_card_roots_toFinset_eq_of_card_aroots_le {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {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).aroots ℂ).toFinset.card ≤ ((F x₀).aroots ℂ).toFinset.card) : ∀ᶠ (x : B) in nhds x₀, (F x).roots.toFinset.card = (F x₀).roots.toFinset.card

Local constancy of the number of real roots. Let F x be real 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 complex roots as F x₀. Then for x near x₀ the polynomials F x and F x₀ have the same number of distinct real roots.