Sturm–Tarski on closed half-lines

The sign sum on [a, ∞) is V(a⁺) - V(+∞) plus the query sign at a if a is a root. Likewise the sign sum on (-∞, b] is V(-∞) - V(b⁻) plus the endpoint contribution. These formulas complement the open half-line formulas in Sturm.Infinity. They apply to positively scaled signed remainder chains, including singleton chains and chains with a nonconstant terminal common factor. Specializing to Polynomial.sturmSeq computes sign sums and distinct root counts without requiring squarefreeness or excluding endpoint roots.

A nonzero head polynomial is required. In particular, the empty root multiset of the zero polynomial is not interpreted as its zero set. All statements are over an arbitrary ordered real closed field; no Archimedean or completeness assumption is used.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, §2.2.2 (Sturm–Tarski and endpoint contributions).

theorem TauCeti.Sturm.sum_sign_Ici {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)} (h : IsSignedRemainderSeq (p :: cs)) (hseed : IsTarskiSeed p f (cs.head?.getD 0)) (a : R) : (↑(signVariationsRight (p :: cs) a) - ↑(signVariationsAtTop (p :: cs)) + if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) = ∑ r ∈ p.roots.toFinset with a ≤ r, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on [a, ∞), with the contribution of the closed endpoint added explicitly.

theorem TauCeti.Sturm.sum_sign_Iic {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p f : Polynomial R} {cs : List (Polynomial R)} (h : IsSignedRemainderSeq (p :: cs)) (hseed : IsTarskiSeed p f (cs.head?.getD 0)) (b : R) : (↑(signVariationsAtBot (p :: cs)) - ↑(signVariationsLeft (p :: cs) b) + if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) = ∑ r ∈ p.roots.toFinset with r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on (-∞, b], with the contribution of the closed endpoint added explicitly.

theorem TauCeti.Sturm.sum_sign_sturmSeq_Ici {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : p ≠ 0) (f : Polynomial R) (a : R) : (↑(signVariationsRight (p.sturmSeq (f * Polynomial.derivative p)) a) - ↑(signVariationsAtTop (p.sturmSeq (f * Polynomial.derivative p))) + if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) = ∑ r ∈ p.roots.toFinset with a ≤ r, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for Mathlib's signed remainder sequence on [a, ∞).

theorem TauCeti.Sturm.sum_sign_sturmSeq_Iic {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : p ≠ 0) (f : Polynomial R) (b : R) : (↑(signVariationsAtBot (p.sturmSeq (f * Polynomial.derivative p))) - ↑(signVariationsLeft (p.sturmSeq (f * Polynomial.derivative p)) b) + if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) = ∑ r ∈ p.roots.toFinset with r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for Mathlib's signed remainder sequence on (-∞, b].

theorem TauCeti.Sturm.card_roots_toFinset_Ici {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : p ≠ 0) (a : R) : (↑(signVariationsRight (p.sturmSeq (Polynomial.derivative p)) a) - ↑(signVariationsAtTop (p.sturmSeq (Polynomial.derivative p))) + if Polynomial.eval a p = 0 then 1 else 0) = ↑{x ∈ p.roots.toFinset | a ≤ x}.card

Sturm counting of distinct roots in [a, ∞), including a possible root at a.

theorem TauCeti.Sturm.card_roots_toFinset_Iic {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : p ≠ 0) (b : R) : (↑(signVariationsAtBot (p.sturmSeq (Polynomial.derivative p))) - ↑(signVariationsLeft (p.sturmSeq (Polynomial.derivative p)) b) + if Polynomial.eval b p = 0 then 1 else 0) = ↑{x ∈ p.roots.toFinset | x ≤ b}.card

Sturm counting of distinct roots in (-∞, b], including a possible root at b.