Root counts of polynomial families are semialgebraic

A polynomial P : (MvPolynomial σ R)[X] is a family of univariate polynomials P.map (MvPolynomial.eval x) parametrized by x : σ → R. This file shows that the number of distinct roots of the specialized polynomial, and the number of its distinct roots below a point t = T(x) given by a polynomial T, are described by finitely many polynomial sign conditions on the parameters. So the sets of parameters with a prescribed count are semialgebraic. In the cylinder coordinates of TauCeti.cylinder, this describes, without any projection, the loci of a family over R ^ n where the distinguished coordinate is a root, respectively not a root, with a prescribed number of roots below it. Over base points where the family does not specialize to zero, these are the graph of the i-th distinct root and the j-th sector, where the sectors are counted from below and include the two unbounded outer sectors.

The specialized degree is described by the vanishing of the coefficients of P. Where it equals d, the specialization is the specialization of the reductum of P below d + 1, and the formal bounds d and d - 1 of this reductum and its derivative are the actual degrees there. Their signed principal subresultant coefficients are polynomials in the parameters, and the number of distinct roots is the permanences minus variations of their values (Polynomial.card_roots_toFinset_eq_permanencesMinusVariations_signedPsc). Roots below t are counted as roots of p.comp (C t - X ^ 2) (Polynomial.card_roots_toFinset_comp_C_sub_X_sq), whose coefficients are again polynomials in the parameters.

Zero specializations, whose zero set is the whole line, are separated explicitly. By convention their Polynomial.roots is empty, so they lie in the sets with count zero.

Main declarations

• TauCeti.isSemialgebraic_setOf_map_eval_eq_zero, TauCeti.isSemialgebraic_setOf_natDegree_map_eval_eq: the parameters with a zero specialization, and with a prescribed specialized degree.
• TauCeti.isSemialgebraic_setOf_card_roots_map_eval: the parameters whose specialization has a prescribed number of distinct roots.
• TauCeti.isSemialgebraic_setOf_card_roots_map_eval_lt: the parameters whose specialization has a prescribed number of distinct roots below T(x).
• TauCeti.isSemialgebraic_setOf_mem_roots_card_roots_lt_and_eval_eq: equality of a polynomial threshold with the distinct root of a prescribed zero-based index.
• TauCeti.isSemialgebraic_setOf_isRoot_card_roots_lt, TauCeti.isSemialgebraic_setOf_not_isRoot_card_roots_lt: the root locus with i roots below and the non-root locus with j roots below of a family over R ^ n, as subsets of R ^ (n + 1). Over nonzero fibers these are the graph of the i-th root and the j-th sector.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapters 4 and 10 (root counting by signed subresultants and uniform sign descriptions).

theorem TauCeti.isSemialgebraic_setOf_map_eval_eq_zero {σ : Type u_1} {R : Type u_2} [CommRing R] [LinearOrder R] (P : Polynomial (MvPolynomial σ R)) : IsSemialgebraic {x : σ → R | Polynomial.map (MvPolynomial.eval x) P = 0}

The parameters at which a polynomial family specializes to zero form a semialgebraic set.

theorem TauCeti.isSemialgebraic_setOf_natDegree_map_eval_le {σ : Type u_1} {R : Type u_2} [CommRing R] [LinearOrder R] (P : Polynomial (MvPolynomial σ R)) (d : ℕ) : IsSemialgebraic {x : σ → R | (Polynomial.map (MvPolynomial.eval x) P).natDegree ≤ d}

The parameters at which the specialization of a polynomial family has degree at most d form a semialgebraic set.

theorem TauCeti.isSemialgebraic_setOf_natDegree_map_eval_eq {σ : Type u_1} {R : Type u_2} [CommRing R] [LinearOrder R] (P : Polynomial (MvPolynomial σ R)) (d : ℕ) : IsSemialgebraic {x : σ → R | (Polynomial.map (MvPolynomial.eval x) P).natDegree = d}

The parameters at which the specialization of a polynomial family has degree exactly d form a semialgebraic set. The zero specializations have degree 0.

theorem TauCeti.isSemialgebraic_setOf_card_roots_map_eval {σ : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (P : Polynomial (MvPolynomial σ R)) (k : ℕ) : IsSemialgebraic {x : σ → R | (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset.card = k}

Uniform root count. The parameters at which the specialization of a polynomial family has exactly k distinct roots form a semialgebraic set. A zero specialization has no roots in Polynomial.roots, so it counts towards k = 0; the zero specializations themselves form the semialgebraic set of TauCeti.isSemialgebraic_setOf_map_eval_eq_zero.

theorem TauCeti.isSemialgebraic_setOf_card_roots_map_eval_lt {σ : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (P : Polynomial (MvPolynomial σ R)) (T : MvPolynomial σ R) (k : ℕ) : IsSemialgebraic {x : σ → R | {r ∈ (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset | r < (MvPolynomial.eval x) T}.card = k}

Uniform count of the roots below a point. For polynomials P and T, the parameters x at which the specialization of P has exactly k distinct roots below T(x) form a semialgebraic set. A zero specialization has no roots in Polynomial.roots, so it counts towards k = 0.

theorem TauCeti.isSemialgebraic_setOf_mem_roots_card_roots_lt_and_eval_eq {σ : Type u_1} {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (P : Polynomial (MvPolynomial σ R)) (T : MvPolynomial σ R) (i : ℕ) : IsSemialgebraic {x : σ → R | ∃ r ∈ (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset, {z ∈ (Polynomial.map (MvPolynomial.eval x) P).roots.toFinset | z < r}.card = i ∧ (MvPolynomial.eval x) T = r}

Equality with the i-th distinct root. For polynomials P and T, the parameters x at which P.map (MvPolynomial.eval x) has an i-th distinct root r (with i distinct roots strictly below r, so i = 0 is the smallest root) and MvPolynomial.eval x T = r form a semialgebraic set.

Roots and sectors in cylinder coordinates

A family P : (MvPolynomial (Fin n) R)[X] over R ^ n has its root graphs and sectors in R ^ (n + 1), with the distinguished coordinate 0 as for TauCeti.cylinder. Over a base point where the specialization at Fin.tail y is nonzero, a point y lies on the graph of the i-th distinct root of P (counted from 0) when y 0 is a root with exactly i roots below it, and in the j-th sector when y 0 is not a root and has exactly j roots below it. The sectors are counted from below: sector 0 lies below the smallest root, the last one above the largest root, and over a fiber without roots sector 0 is the whole fiber. Over a base point where P specializes to zero, the root predicate holds on the whole fiber for i = 0 and nowhere else, and the non-root predicate holds nowhere.

theorem TauCeti.isSemialgebraic_setOf_isRoot_card_roots_lt {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {n : ℕ} (P : Polynomial (MvPolynomial (Fin n) R)) (i : ℕ) : IsSemialgebraic {y : Fin (n + 1) → R | (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).IsRoot (y 0) ∧ {r ∈ (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset | r < y 0}.card = i}

The root locus with i roots below. The points of R ^ (n + 1) whose coordinate 0 is a root of the specialization of P at the remaining coordinates, with exactly i distinct roots below it, form a semialgebraic set. Over a base point where P does not specialize to zero, this is the graph of the i-th distinct root (counted from 0). Over a base point where P specializes to zero, it is the whole fiber for i = 0 and empty otherwise.

theorem TauCeti.isSemialgebraic_setOf_not_isRoot_card_roots_lt {R : Type u_2} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {n : ℕ} (P : Polynomial (MvPolynomial (Fin n) R)) (j : ℕ) : IsSemialgebraic {y : Fin (n + 1) → R | ¬(Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).IsRoot (y 0) ∧ {r ∈ (Polynomial.map (MvPolynomial.eval (Fin.tail y)) P).roots.toFinset | r < y 0}.card = j}

The non-root locus with j roots below. The points of R ^ (n + 1) whose coordinate 0 is not a root of the specialization of P at the remaining coordinates, with exactly j distinct roots below it, form a semialgebraic set. Over a base point where P does not specialize to zero, this is the j-th sector counted from below, including the unbounded sectors below the smallest and above the largest root. Over a base point where P specializes to zero there are no such points.