The sign variations of positive multiples and of polynomials near infinity

Candidates for a file of Mathlib on Sturm's theorem: lists of polynomials over an ordered field that are entrywise positive multiples (Polynomial.PosAssoc), such as a generalized Sturm sequence and the Sturm sequence of its first two entries, have the same sign variations at every point and at ±∞ (Polynomial.signVariations_map_eval_eq_of_forall₂, Polynomial.signVariations_map_leadingCoeff_eq_of_forall₂, Polynomial.signVariations_map_neg_one_pow_mul_leadingCoeff_eq_of_forall₂); and far right, the sign variations of a list of nonzero polynomials at a point are those of their leading coefficients, and far left those of their leading coefficients, each times (-1) ^ deg (Polynomial.eventually_atTop_signVariations, Polynomial.eventually_atBot_signVariations). The image of a rational polynomial in an ordered field has at a rational point the sign of the value of the polynomial (Polynomial.sign_eval_map_ratCastHom), so that a remainder chain computed over ℚ has the signs of its image over ℝ.

Implementation notes

The file has no Mathlib sibling: Mathlib has the Sturm sequence (Mathlib.Algebra.Polynomial.Sturm.Sequence) and the sign variations of a list (Mathlib.Data.List.SignVariations), but neither file imports the other, and Mathlib has neither Sturm's theorem nor a file that imports both. So the file chooses its imports: the sign variations, and the mirrors of the Sturm sequence (Polynomial.PosAssoc) and of the eventual signs of polynomials (Mathlib.Analysis.Polynomial.Order, which brings the filters and the ordered normed fields of the statements), and for its proofs the mirror of Mathlib.Algebra.Polynomial.Eval.Coeff, with the values of the images of polynomials at rational points (Polynomial.eval_ratCast_map).

theorem Polynomial.signVariations_map_eq_of_forall₂ {K : Type u_1} [Field K] [LinearOrder K] {β : Type u_2} [Zero β] [LinearOrder β] {g : Polynomial K → β} (hg : ∀ (p q : Polynomial K), p.PosAssoc q → SignType.sign (g q) = SignType.sign (g p)) {l l' : List (Polynomial K)} (h : List.Forall₂ PosAssoc l l') : (List.map g l').signVariations = (List.map g l).signVariations

Lists of polynomials that are entrywise positive multiples have the same sign variations under every map g to a linear order that keeps the signs of positive multiples, such as the evaluation at a point and the leading coefficient.

theorem Polynomial.PosAssoc.sign_eval {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {p q : Polynomial K} (h : p.PosAssoc q) (x : K) : SignType.sign (eval x q) = SignType.sign (eval x p)

theorem Polynomial.PosAssoc.sign_leadingCoeff {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {p q : Polynomial K} (h : p.PosAssoc q) : SignType.sign q.leadingCoeff = SignType.sign p.leadingCoeff

theorem Polynomial.signVariations_map_eval_eq_of_forall₂ {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {l l' : List (Polynomial K)} (h : List.Forall₂ PosAssoc l l') (x : K) : (List.map (eval x) l').signVariations = (List.map (eval x) l).signVariations

Lists of polynomials that are entrywise positive multiples have the same sign variations at every point.

theorem Polynomial.signVariations_map_leadingCoeff_eq_of_forall₂ {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {l l' : List (Polynomial K)} (h : List.Forall₂ PosAssoc l l') : (List.map leadingCoeff l').signVariations = (List.map leadingCoeff l).signVariations

Lists of polynomials that are entrywise positive multiples have the same sign variations of their leading coefficients, the count at +∞.

theorem Polynomial.signVariations_map_neg_one_pow_mul_leadingCoeff_eq_of_forall₂ {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] {l l' : List (Polynomial K)} (h : List.Forall₂ PosAssoc l l') : (List.map (fun (p : Polynomial K) => (-1) ^ p.natDegree * p.leadingCoeff) l').signVariations = (List.map (fun (p : Polynomial K) => (-1) ^ p.natDegree * p.leadingCoeff) l).signVariations

Lists of polynomials that are entrywise positive multiples have the same sign variations of their leading coefficients times (-1) ^ deg, the count at -∞.

theorem Polynomial.eventually_atTop_signVariations {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {ps : List (Polynomial 𝕜)} (h : ∀ p ∈ ps, p ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atTop, (List.map (eval x) ps).signVariations = (List.map leadingCoeff ps).signVariations

Far right, the sign variations of a list of nonzero polynomials at a point are those of their leading coefficients.

theorem Polynomial.eventually_atBot_signVariations {𝕜 : Type u_1} [NormedField 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [OrderTopology 𝕜] {ps : List (Polynomial 𝕜)} (h : ∀ p ∈ ps, p ≠ 0) : ∀ᶠ (x : 𝕜) in Filter.atBot, (List.map (eval x) ps).signVariations = (List.map (fun (p : Polynomial 𝕜) => (-1) ^ p.natDegree * p.leadingCoeff) ps).signVariations

Far left, the sign variations of a list of nonzero polynomials at a point are those of their leading coefficients, each times (-1) ^ deg.

theorem Polynomial.sign_eval_map_ratCastHom {K : Type u_1} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (p : Polynomial ℚ) (q : ℚ) : SignType.sign (eval (↑q) (map (Rat.castHom K) p)) = SignType.sign (eval q p)

The sign of the value of the image of a rational polynomial in an ordered field at a rational point is the sign of the value of the polynomial.