Sturm–Tarski over an arbitrary real closed ordered field

IsTarskiSeed relates the second chain entry to f * p' modulo p. sum_sign identifies the variation difference of a signed remainder chain with the sum of query signs at the distinct roots in an open interval. Positive pseudo-remainder scalings and a nonconstant terminal common factor are allowed, and the head polynomial need not be squarefree. IsTarskiSeed.sign_eq_of_mul, IsTarskiSeed.eval_eq_zero_of_mul, IsTarskiSeed.derivative_eval_ne_zero_of_mul and IsTarskiSeed.sign_mul_eq_of_mul describe the query at the roots of a seed from which a common factor of the head and second entry has been removed; IsTarskiSeed.sign_eq and IsTarskiSeed.eval_eq_zero are the forms without a common factor. The concrete Polynomial.sturmSeq specialization supplies sign sums and root counts, and is the finite-interval basis for the infinite-endpoint formulas.

References

For the classical sign-sum identity, see S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, revised second edition, §2.2.2, Theorem 2.73 (Tarski’s theorem).

def TauCeti.Sturm.IsTarskiSeed {R : Type u_1} [Field R] [LinearOrder R] (p f q : Polynomial R) : Prop

The positive-scaled seed congruence between the second entry and f * p' modulo p. Both scalings are explicit to cover signed pseudo-remainders. A degree bound identifies the actual remainder, but is unnecessary for soundness.

Equations

• TauCeti.Sturm.IsTarskiSeed p f q = TauCeti.Sturm.IsRemainder (f * Polynomial.derivative p) p (-q)

theorem TauCeti.Sturm.IsTarskiSeed.of_identity {R : Type u_1} [Field R] [LinearOrder R] {p f q : Polynomial R} (a b : R) (u : Polynomial R) (ha : 0 < a) (hb : 0 < b) (heq : Polynomial.C a * (f * Polynomial.derivative p) = u * p + Polynomial.C b * q) : IsTarskiSeed p f q

Construct a query seed from its positive-scaled congruence identity.

theorem TauCeti.Sturm.IsTarskiSeed.exists_identity {R : Type u_1} [Field R] [LinearOrder R] {p f q : Polynomial R} (h : IsTarskiSeed p f q) : ∃ (a : R) (b : R) (u : Polynomial R), 0 < a ∧ 0 < b ∧ Polynomial.C a * (f * Polynomial.derivative p) = u * p + Polynomial.C b * q

A query seed supplies positive scalings and the congruence identity.

theorem TauCeti.Sturm.IsTarskiSeed.mul_derivative {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p f : Polynomial R) : IsTarskiSeed p f (f * Polynomial.derivative p)

The unreduced derivative query is a valid Tarski seed.

theorem TauCeti.Sturm.IsTarskiSeed.mod {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (p f : Polynomial R) : IsTarskiSeed p f (f * Polynomial.derivative p % p)

Reducing the derivative query modulo the head gives a valid Tarski seed.

theorem TauCeti.Sturm.IsTarskiSeed.sign_eq_of_mul {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {d p f q : Polynomial R} (h : IsTarskiSeed (d * p) f (d * q)) (hd : d ≠ 0) {r : R} (hr : Polynomial.eval r p = 0) : SignType.sign (Polynomial.eval r (Polynomial.derivative p) * Polynomial.eval r f) = SignType.sign (Polynomial.eval r q)

If q is a Tarski seed for the head d * p and query f after the common factor d is removed from it, then at every root r of p the sign of p' r * f r is the sign of q r. The point r may be a multiple root of d * p.

theorem TauCeti.Sturm.IsTarskiSeed.eval_eq_zero_of_mul {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {d p f q : Polynomial R} (h : IsTarskiSeed (d * p) f (d * q)) (hd : d ≠ 0) {r : R} (hdr : Polynomial.eval r d = 0) (hp : Polynomial.eval r p ≠ 0) : Polynomial.eval r f = 0

A root of the removed common factor d that is not a root of the reduced head p is a zero of the query.

theorem TauCeti.Sturm.IsTarskiSeed.derivative_eval_ne_zero_of_mul {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {d p f q : Polynomial R} (h : IsTarskiSeed (d * p) f (d * q)) (hd : d ≠ 0) {r : R} (hr : Polynomial.eval r p = 0) (hq : Polynomial.eval r q ≠ 0) : Polynomial.eval r (Polynomial.derivative p) ≠ 0

At a root r of the reduced head p at which the reduced second entry q does not vanish, r is a simple root of p. This holds even if r is a multiple root of d * p.

theorem TauCeti.Sturm.IsTarskiSeed.sign_mul_eq_of_mul {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {d p f q : Polynomial R} (h : IsTarskiSeed (d * p) f (d * q)) (hd : d ≠ 0) {r : R} (hr : Polynomial.eval r p = 0) (hq : Polynomial.eval r q ≠ 0) : SignType.sign (Polynomial.eval r (Polynomial.derivative p) * Polynomial.eval r q) = SignType.sign (Polynomial.eval r f)

At a root r of the reduced head p at which the reduced second entry q does not vanish, the sign of p' r * q r is the sign of the query f r.

theorem TauCeti.Sturm.IsTarskiSeed.sign_eq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p f q : Polynomial R} (h : IsTarskiSeed p f q) {r : R} (hr : Polynomial.eval r p = 0) : SignType.sign (Polynomial.eval r (Polynomial.derivative p) * Polynomial.eval r f) = SignType.sign (Polynomial.eval r q)

At every root r of the head p of a Tarski seed, the sign of p' r * f r is the sign of q r. The point r may be a multiple root of p.

theorem TauCeti.Sturm.IsTarskiSeed.eval_eq_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p f : Polynomial R} (h : IsTarskiSeed p f 0) (hp : p ≠ 0) {r : R} (hr : Polynomial.eval r p = 0) : Polynomial.eval r f = 0

A zero query seed makes the query vanish at every root of the nonzero head.

theorem TauCeti.Sturm.IsTarskiSeed.sturmSeq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p f q : Polynomial R} (h : IsTarskiSeed p f q) : IsTarskiSeed p f ((p.sturmSeq q).tail.head?.getD 0)

A valid query seed remains valid as the second entry of Mathlib's sequence, including the singleton case.

theorem TauCeti.Sturm.IsTarskiSeed.sum_sign_eq_zero {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {p f : Polynomial R} (hseed : IsTarskiSeed p f 0) (hp : p ≠ 0) (Z : Finset R) (hZ : ∀ r ∈ Z, Polynomial.eval r p = 0) : ∑ r ∈ Z, ↑(SignType.sign (Polynomial.eval r f)) = 0

A zero query seed makes the query vanish at every root of the nonzero head, so its sign sum is zero on any finite set of such roots.

theorem TauCeti.Sturm.sum_sign {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 b : R} (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : ↑(signVariationsAt (p :: cs) a) - ↑(signVariationsAt (p :: cs) b) = ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for any nonempty signed remainder chain, including a singleton. The seed is the second entry, or zero when the chain has only its head. The head polynomial may have multiple roots.

theorem TauCeti.Sturm.sum_sign_sturmSeq {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p f : Polynomial R) {a b : R} (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : ↑(signVariationsAt (p.sturmSeq (f * Polynomial.derivative p)) a) - ↑(signVariationsAt (p.sturmSeq (f * Polynomial.derivative p)) b) = ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski directly for Mathlib's concrete signed remainder sequence.

theorem TauCeti.Sturm.card_roots_toFinset {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) {a b : R} (hab : a < b) (ha : Polynomial.eval a p ≠ 0) (hb : Polynomial.eval b p ≠ 0) : ↑(signVariationsAt (p.sturmSeq (Polynomial.derivative p)) a) - ↑(signVariationsAt (p.sturmSeq (Polynomial.derivative p)) b) = ↑{r ∈ p.roots.toFinset | a < r ∧ r < b}.card

Classical Sturm counting of distinct roots in (a, b), counted without multiplicity. Neither endpoint may be a root.