Common root matching for finite families of polynomials

Let F k x, for k in a finite index type, be polynomials over a proper algebraically closed normed field whose coefficients depend continuously on a parameter x, each of fixed degree. For a single member, Polynomial.eventually_exists_bijOn_roots_toFinset matches the distinct roots of F k x with those of F k x₀, preserving multiplicities, as long as the number of distinct roots does not increase near x₀. Separate matchings need not be compatible: two members sharing a root at x₀ could have nearby roots that drift apart.

This file shows that if, in addition, the degree of the gcd of every pair of members is locally constant, then one bijection between the union of the distinct roots of the members at x₀ and at x works for all members simultaneously. It moves each root by less than a prescribed ε and preserves its multiplicity in every member; in particular it preserves membership in every root set. Consequently the total number of distinct roots of the family is locally constant.

Only pairwise gcd data are needed. The persistence of a common root of two members comes from TauCeti.eventually_exists_common_root_norm_sub_lt; the individual matchings then force every nearby common root to be the partner of the central root in both members.

Main results

• Polynomial.eventually_exists_bijOn_biUnion_roots_toFinset: the family matching lemma.
• Polynomial.eventually_card_biUnion_roots_toFinset_eq: local constancy of the number of distinct roots of the family.

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_roots_toFinset {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {B : Type u_2} [TopologicalSpace B] {ι : Type u_3} [Fintype ι] {F : ι → B → Polynomial K} {x₀ : B} {d : ι → ℕ} (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).roots.toFinset.card ≤ (F k x₀).roots.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 : K → K), Set.BijOn e ↑(Finset.univ.biUnion fun (k : ι) => (F k x₀).roots.toFinset) ↑(Finset.univ.biUnion fun (k : ι) => (F k x).roots.toFinset) ∧ ∀ z ∈ Finset.univ.biUnion fun (k : ι) => (F k x₀).roots.toFinset, ‖e z - z‖ < ε ∧ ∀ (k : ι), rootMultiplicity (e z) (F k x) = rootMultiplicity z (F k x₀)

Family matching lemma. Let F k x be 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 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 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_biUnion_roots_toFinset_eq {K : Type u_1} [NormedField K] [IsAlgClosed K] [ProperSpace K] {B : Type u_2} [TopologicalSpace B] {ι : Type u_3} [Fintype ι] {F : ι → B → Polynomial K} {x₀ : B} {d : ι → ℕ} (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).roots.toFinset.card ≤ (F k x₀).roots.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₀, (Finset.univ.biUnion fun (k : ι) => (F k x).roots.toFinset).card = (Finset.univ.biUnion fun (k : ι) => (F k x₀).roots.toFinset).card

Local constancy of the number of distinct roots of a family. Under the hypotheses of the family matching lemma, the members of the family have, together, as many distinct roots near x₀ as at x₀.