Ordered real roots in continuous polynomial families

For a real polynomial family of fixed degree with continuous coefficients, a locally nonincreasing number of distinct complex roots forces its increasing enumeration of real roots to vary continuously. The multiplicity at each position is locally constant. On a preconnected base, both the number of real roots and their ordered multiplicities are constant, so a single finite ordered list gives continuous root functions on the whole base.

The local statements require a strictly increasing complete enumeration only near the parameter, without assuming its continuity. The connected existence theorem constructs it using Mathlib's Finset.orderEmbOfFin, and excludes zero fibers by its fixed-degree hypothesis. Constant polynomials and empty root lists are included.

References

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

theorem Polynomial.eventually_ordered_roots_close_of_card_aroots_le {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {d n : ℕ} {x₀ : B} (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) {r : B → Fin n → ℝ} (hr : ∀ᶠ (x : B) in nhds x₀, StrictMono (r x)) (hroots : ∀ᶠ (x : B) in nhds x₀, Set.range (r x) = ↑(F x).roots.toFinset) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∀ (i : Fin n), |r x i - r x₀ i| < ε ∧ rootMultiplicity (r x i) (F x) = rootMultiplicity (r x₀ i) (F x₀)

An increasing complete enumeration of the distinct real roots moves arbitrarily little near x₀ and preserves multiplicities, when the coefficients are continuous, the degree is locally fixed, and the number of distinct complex roots is locally nonincreasing. The enumeration is required to be increasing and complete only near x₀; no continuity is assumed.

theorem Polynomial.continuousAt_ordered_root_of_card_aroots_le {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {d n : ℕ} {x₀ : B} (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) {r : B → Fin n → ℝ} (hr : ∀ᶠ (x : B) in nhds x₀, StrictMono (r x)) (hroots : ∀ᶠ (x : B) in nhds x₀, Set.range (r x) = ↑(F x).roots.toFinset) (i : Fin n) : ContinuousAt (fun (x : B) => r x i) x₀

Every position in an increasing complete enumeration of real roots is continuous at a parameter where the coefficients are continuous, the degree is locally fixed, and the number of distinct complex roots is locally nonincreasing. The enumeration is required to be increasing and complete only near that parameter.

theorem Polynomial.isLocallyConstant_rootMultiplicity_ordered_root_of_card_aroots_le {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {d n : ℕ} (hF : ∀ i ≤ d, Continuous fun (x : B) => (F x).coeff i) (hdeg : ∀ (x : B), (F x).degree = ↑d) (hcard : ∀ (x₀ : B), ∀ᶠ (x : B) in nhds x₀, ((F x).aroots ℂ).toFinset.card ≤ ((F x₀).aroots ℂ).toFinset.card) {r : B → Fin n → ℝ} (hr : ∀ (x : B), StrictMono (r x)) (hroots : ∀ (x : B), Set.range (r x) = ↑(F x).roots.toFinset) (i : Fin n) : IsLocallyConstant fun (x : B) => rootMultiplicity (r x i) (F x)

Multiplicity at each position in an increasing complete enumeration of real roots is locally constant, provided the coefficient and root-count hypotheses hold at every parameter.

theorem Polynomial.card_roots_toFinset_eq_of_preconnectedSpace {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {d : ℕ} [PreconnectedSpace B] (hF : ∀ i ≤ d, Continuous fun (x : B) => (F x).coeff i) (hdeg : ∀ (x : B), (F x).degree = ↑d) (hcard : ∀ (x₀ : B), ∀ᶠ (x : B) in nhds x₀, ((F x).aroots ℂ).toFinset.card ≤ ((F x₀).aroots ℂ).toFinset.card) (x y : B) : (F x).roots.toFinset.card = (F y).roots.toFinset.card

The number of distinct real roots is constant on a preconnected base if the degree is fixed, the coefficients are continuous, and the number of distinct complex roots is locally nonincreasing.

theorem Polynomial.exists_continuous_ordered_roots_of_preconnectedSpace {B : Type u_1} [TopologicalSpace B] {F : B → Polynomial ℝ} {d : ℕ} [PreconnectedSpace B] [Nonempty B] (hF : ∀ i ≤ d, Continuous fun (x : B) => (F x).coeff i) (hdeg : ∀ (x : B), (F x).degree = ↑d) (hcard : ∀ (x₀ : B), ∀ᶠ (x : B) in nhds x₀, ((F x).aroots ℂ).toFinset.card ≤ ((F x₀).aroots ℂ).toFinset.card) : ∃ (n : ℕ) (r : B → Fin n → ℝ), (∀ (i : Fin n), Continuous fun (x : B) => r x i) ∧ (∀ (x : B), StrictMono (r x)) ∧ (∀ (x : B) (t : ℝ), (F x).IsRoot t ↔ ∃ (i : Fin n), r x i = t) ∧ ∀ (i : Fin n) (x y : B), rootMultiplicity (r x i) (F x) = rootMultiplicity (r y i) (F y)

On a nonempty preconnected base, a fixed-degree continuous polynomial family with locally nonincreasing number of distinct complex roots has a global finite increasing enumeration of all its real zeros by continuous functions. The multiplicity at each position is constant. No fixed real root count or continuous root enumeration is assumed.