Common ordered real roots of a finite family of real polynomials

Let F k x, for k in a finite index type, be real polynomials of fixed degrees whose coefficients depend continuously on a parameter x. Suppose that the number of distinct complex roots of each member is locally nonincreasing and that the degree of the gcd of every pair of distinct members is locally constant. The family matching lemma Polynomial.eventually_exists_bijOn_biUnion_roots_toFinset then shows that the product of the members has a locally constant number of distinct complex roots, so the results of TauCeti/Analysis/Polynomial/RealRoots/Ordered.lean apply to the product.

On a nonempty preconnected base this gives a single finite list of continuous, strictly increasing functions enumerating, at every parameter, the real roots of all the members together, such that the multiplicity of each listed root in each member is the same at every parameter. In particular membership of a listed root in the root set of each member does not depend on the parameter. This is the common ordered list of real roots over which a delineable family is stacked.

Main results

• Polynomial.eventually_card_aroots_prod_eq: the product of the members has locally constant number of distinct complex roots.
• Polynomial.exists_continuous_ordered_common_roots_of_preconnectedSpace: the common ordered list of real roots with constant multiplicities in every member.

References

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

theorem Polynomial.eventually_exists_bijOn_biUnion_aroots_toFinset {B : Type u_1} [TopologicalSpace B] {ι : Type u_2} [Fintype ι] {F : ι → B → Polynomial ℝ} {d : ι → ℕ} {x₀ : B} (hF : ∀ (k : ι), ∀ i ≤ d k, ContinuousAt (fun (x : B) => (F k x).coeff i) x₀) (hdeg : ∀ (k : ι), ∀ᶠ (x : B) in nhds x₀, (F k x).degree = ↑(d k)) (hcard : ∀ (k : ι), ∀ᶠ (x : B) in nhds x₀, ((F k x).aroots ℂ).toFinset.card ≤ ((F k x₀).aroots ℂ).toFinset.card) (hgcd : Pairwise fun (k l : ι) => ∀ᶠ (x : B) in nhds x₀, (EuclideanDomain.gcd (F k x) (F l x)).natDegree = (EuclideanDomain.gcd (F k x₀) (F l x₀)).natDegree) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (x : B) in nhds x₀, ∃ (e : ℂ → ℂ), Set.BijOn e ↑(Finset.univ.biUnion fun (k : ι) => ((F k x₀).aroots ℂ).toFinset) ↑(Finset.univ.biUnion fun (k : ι) => ((F k x).aroots ℂ).toFinset) ∧ ∀ z ∈ Finset.univ.biUnion fun (k : ι) => ((F k x₀).aroots ℂ).toFinset, ‖e z - z‖ < ε ∧ ∀ (k : ι), rootMultiplicity (e z) (map (algebraMap ℝ ℂ) (F k x)) = rootMultiplicity z (map (algebraMap ℝ ℂ) (F k x₀))

Family matching lemma for real polynomials. Let F k x be real polynomials of degree d k near x₀, for k in a finite index type, whose coefficients of index at most d k are continuous at x₀. Suppose that near x₀ no member has more distinct complex roots than at x₀, and that the degree of the gcd of every pair of distinct members is the same as at x₀. Then for x near x₀ there is a single bijection e from the distinct complex roots of all the F k x₀ onto those of all the F k x that moves each root by less than ε and preserves its multiplicity in every member.

theorem Polynomial.eventually_card_aroots_prod_eq {B : Type u_1} [TopologicalSpace B] {ι : Type u_2} [Fintype ι] {F : ι → B → Polynomial ℝ} {d : ι → ℕ} {x₀ : B} (hF : ∀ (k : ι), ∀ i ≤ d k, ContinuousAt (fun (x : B) => (F k x).coeff i) x₀) (hdeg : ∀ (k : ι), ∀ᶠ (x : B) in nhds x₀, (F k x).degree = ↑(d k)) (hcard : ∀ (k : ι), ∀ᶠ (x : B) in nhds x₀, ((F k x).aroots ℂ).toFinset.card ≤ ((F k x₀).aroots ℂ).toFinset.card) (hgcd : Pairwise fun (k l : ι) => ∀ᶠ (x : B) in nhds x₀, (EuclideanDomain.gcd (F k x) (F l x)).natDegree = (EuclideanDomain.gcd (F k x₀) (F l x₀)).natDegree) : ∀ᶠ (x : B) in nhds x₀, ((∏ k : ι, F k x).aroots ℂ).toFinset.card = ((∏ k : ι, F k x₀).aroots ℂ).toFinset.card

Distinct complex roots of the product of a family. Under the hypotheses of the family matching lemma for real polynomials, the product of the members has, near x₀, as many distinct complex roots as at x₀.

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

Common ordered real roots. Let F k x be real polynomials of degree d k, for k in a finite index type, whose coefficients depend continuously on a parameter in a nonempty preconnected space. Suppose that the number of distinct complex roots of each member is locally nonincreasing, and the degree of the gcd of every pair of distinct members is locally constant. Then there are finitely many continuous functions r x 0 < ⋯ < r x (n - 1) whose values at each x are exactly the real roots of the members F k x together, and the multiplicity of r x i as a root of each member F k x does not depend on x.