Cauchy indices from signed subresultant coefficients

Let p and q be polynomials over an ordered real closed field with q.natDegree < p.natDegree = m, and let s_j = signedPsc p q m q.natDegree j be their signed principal subresultant coefficients at the actual degrees. The permanences minus variations of the list [s_m, …, s_0] is the Cauchy index of q / p on the whole line. Applied to suitable pairs, this computes roots and Tarski queries from signs of principal subresultant coefficients, which are polynomials in the coefficients of the pair: the number of distinct roots of p uses the pair (p, derivative p), and the Tarski query of q at the roots of p uses the pair (p, derivative p * q % p).

The proof follows the signed remainder sequence p, q, -(p % q), …. One Euclidean step multiplies the signed coefficients of index at most (p % q).natDegree by a common nonzero constant (Polynomial.signedPsc_eq_mul_signedPsc_neg_mod), and the coefficients of larger index below q.natDegree vanish (Polynomial.signedPsc_eq_zero_of_natDegree_mod_lt). On the Cauchy-index side, the same step changes the whole-line index by the contribution of the leading pair.

Main declarations

• Polynomial.cauchyIndex_univ_eq_permanencesMinusVariations_signedPsc: the Cauchy index of q / p is permanences minus variations of the signed principal coefficients.
• Polynomial.cauchyIndex_univ_eq_permanencesMinusVariations_signedPsc_mod: the same for an arbitrary numerator, reduced modulo p.
• Polynomial.tarskiQuery_eq_permanencesMinusVariations_signedPsc, Polynomial.card_roots_toFinset_eq_permanencesMinusVariations_signedPsc: Tarski queries and the number of distinct roots from principal coefficients.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, Chapter 4 (signed subresultants and the Cauchy index).

theorem Polynomial.cauchyIndex_univ_eq_permanencesMinusVariations_signedPsc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p q : Polynomial R} (h : q.natDegree < p.natDegree) : p.cauchyIndex q Set.univ = (List.map (p.signedPsc q p.natDegree q.natDegree) (List.range (p.natDegree + 1)).reverse).permanencesMinusVariations

Cauchy index by signed subresultants. For q.natDegree < p.natDegree = m, the whole-line Cauchy index of q / p is the permanences minus variations of the signed principal subresultant coefficients [s_m, …, s_0] of p and q at their actual degrees. The numerator may be zero, and p and q may have common factors and multiple roots.

theorem Polynomial.cauchyIndex_univ_eq_permanencesMinusVariations_signedPsc_mod {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p q : Polynomial R) : p.cauchyIndex q Set.univ = (List.map (p.signedPsc (q % p) p.natDegree (q % p).natDegree) (List.range (p.natDegree + 1)).reverse).permanencesMinusVariations

Cauchy index by signed subresultants, general numerator. Reducing q modulo p does not change the Cauchy index of q / p, so it is the permanences minus variations of the signed principal subresultant coefficients of p and q % p. For constant p both sides vanish.

theorem Polynomial.tarskiQuery_eq_permanencesMinusVariations_signedPsc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p q : Polynomial R) : p.tarskiQuery q = (List.map (p.signedPsc (derivative p * q % p) p.natDegree (derivative p * q % p).natDegree) (List.range (p.natDegree + 1)).reverse).permanencesMinusVariations

The Tarski query of q at the roots of p is the permanences minus variations of the signed principal subresultant coefficients of p and p' * q % p.

theorem Polynomial.card_roots_toFinset_eq_permanencesMinusVariations_signedPsc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) : ↑p.roots.toFinset.card = (List.map (p.signedPsc (derivative p) p.natDegree (derivative p).natDegree) (List.range (p.natDegree + 1)).reverse).permanencesMinusVariations

The number of distinct roots of p is the permanences minus variations of the signed principal subresultant coefficients of p and its derivative.