Sturm–Tarski with one-sided endpoints

TauCeti.Sturm.signVariationsRight cs a and TauCeti.Sturm.signVariationsLeft cs a count the sign variations of a polynomial list immediately to the right and to the left of a. They are computed algebraically from the one-sided signs Polynomial.signRight and Polynomial.signLeft, and are realized by evaluation at every point of a small enough interval on the corresponding side of a.

With these, Sturm–Tarski holds on every bounded interval, with no condition on the endpoints. Write V(a⁺) and V(b⁻) for the right-hand variations at a and the left-hand variations at b of a signed remainder chain whose head is p and whose second entry is the seed of the query f. For a < b, the difference V(a⁺) - V(b⁻) is the sum of the signs of f at the distinct roots of p in (a, b), even when a or b is a root of p or of another chain entry. A root c of p contributes the sign of f at c to a closed endpoint, and this contribution is the drop V(c⁻) - V(c⁺) in variations across c. The formulas for (a, b], [a, b) and [a, b] add these endpoint contributions explicitly to V(a⁺) - V(b⁻). Specializing to Polynomial.sturmSeq and to the query 1 counts distinct roots.

Main declarations

• TauCeti.Sturm.signVariationsRight, TauCeti.Sturm.signVariationsLeft: one-sided variations.
• TauCeti.Sturm.sum_sign_Ioo: Sturm–Tarski on (a, b) as V(a⁺) - V(b⁻).
• TauCeti.Sturm.signVariationsLeft_sub_signVariationsRight: the contribution of a point.
• TauCeti.Sturm.sum_sign_Ioc, TauCeti.Sturm.sum_sign_Ico, TauCeti.Sturm.sum_sign_Icc: Sturm–Tarski on half-open and closed intervals.
• TauCeti.Sturm.card_roots_toFinset_Ioo and its half-open and closed analogues: Sturm's count of distinct roots.

References

S. Basu, R. Pollack, and M.-F. Roy, Algorithms in Real Algebraic Geometry, second edition, §2.2.2 (Tarski's theorem) and Chapter 10.

noncomputable def TauCeti.Sturm.signVariationsRight {R : Type u_1} [CommRing R] [LinearOrder R] (cs : List (Polynomial R)) (a : R) : ℕ

The sign variations of a polynomial list immediately to the right of a: the variations of the right-hand signs Polynomial.signRight of its entries at a.

Equations

• TauCeti.Sturm.signVariationsRight cs a = (List.map (fun (x : Polynomial R) => x.signRight a) cs).signVariations

noncomputable def TauCeti.Sturm.signVariationsLeft {R : Type u_1} [CommRing R] [LinearOrder R] (cs : List (Polynomial R)) (a : R) : ℕ

The sign variations of a polynomial list immediately to the left of a: the variations of the left-hand signs Polynomial.signLeft of its entries at a.

Equations

• TauCeti.Sturm.signVariationsLeft cs a = (List.map (fun (x : Polynomial R) => x.signLeft a) cs).signVariations

theorem TauCeti.Sturm.signVariationsRight_def {R : Type u_1} [CommRing R] [LinearOrder R] (cs : List (Polynomial R)) (a : R) : signVariationsRight cs a = (List.map (fun (x : Polynomial R) => x.signRight a) cs).signVariations

theorem TauCeti.Sturm.signVariationsLeft_def {R : Type u_1} [CommRing R] [LinearOrder R] (cs : List (Polynomial R)) (a : R) : signVariationsLeft cs a = (List.map (fun (x : Polynomial R) => x.signLeft a) cs).signVariations

@[simp]

theorem TauCeti.Sturm.signVariationsRight_nil {R : Type u_1} [CommRing R] [LinearOrder R] (a : R) : signVariationsRight [] a = 0

@[simp]

theorem TauCeti.Sturm.signVariationsLeft_nil {R : Type u_1} [CommRing R] [LinearOrder R] (a : R) : signVariationsLeft [] a = 0

@[simp]

theorem TauCeti.Sturm.signVariationsRight_singleton {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : signVariationsRight [p] a = 0

@[simp]

theorem TauCeti.Sturm.signVariationsLeft_singleton {R : Type u_1} [CommRing R] [LinearOrder R] (p : Polynomial R) (a : R) : signVariationsLeft [p] a = 0

theorem TauCeti.Sturm.signVariationsAt_eq_right {R : Type u_1} [CommRing R] [LinearOrder R] {cs : List (Polynomial R)} {a x : R} (h : ∀ p ∈ cs, SignType.sign (Polynomial.eval x p) = p.signRight a) : signVariationsAt cs x = signVariationsRight cs a

Evaluation at a point where every entry has its right-hand sign at a realizes the right-hand variations at a.

theorem TauCeti.Sturm.signVariationsAt_eq_left {R : Type u_1} [CommRing R] [LinearOrder R] {cs : List (Polynomial R)} {a x : R} (h : ∀ p ∈ cs, SignType.sign (Polynomial.eval x p) = p.signLeft a) : signVariationsAt cs x = signVariationsLeft cs a

Evaluation at a point where every entry has its left-hand sign at a realizes the left-hand variations at a.

theorem TauCeti.Sturm.signVariationsRight_eq_signVariationsAt {R : Type u_1} [CommRing R] [LinearOrder R] {cs : List (Polynomial R)} {a : R} (h : ∀ p ∈ cs, Polynomial.eval a p ≠ 0) : signVariationsRight cs a = signVariationsAt cs a

If no entry vanishes at a, the right-hand variations are the variations at a.

theorem TauCeti.Sturm.signVariationsLeft_eq_signVariationsAt {R : Type u_1} [CommRing R] [LinearOrder R] {cs : List (Polynomial R)} {a : R} (h : ∀ p ∈ cs, Polynomial.eval a p ≠ 0) : signVariationsLeft cs a = signVariationsAt cs a

If no entry vanishes at a, the left-hand variations are the variations at a.

theorem TauCeti.Sturm.exists_signVariationsRight {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (a : R) : ∃ (u : R), a < u ∧ ∀ x ∈ Set.Ioo a u, signVariationsAt cs x = signVariationsRight cs a

The right-hand variations at a are the variations at every point of a small enough interval to the right of a.

theorem TauCeti.Sturm.exists_signVariationsLeft {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (a : R) : ∃ l < a, ∀ x ∈ Set.Ioo l a, signVariationsAt cs x = signVariationsLeft cs a

The left-hand variations at a are the variations at every point of a small enough interval to the left of a.

theorem TauCeti.Sturm.sum_sign_Ioo {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) : ↑(signVariationsRight (p :: cs) a) - ↑(signVariationsLeft (p :: cs) b) = ∑ r ∈ p.roots.toFinset with a < r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski with one-sided endpoints. For a signed remainder chain with head p and query seed f, and any a < b, the right-hand variations at a minus the left-hand variations at b is the sum of the signs of f at the distinct roots of p in (a, b). The endpoints may be roots of any chain entry.

theorem TauCeti.Sturm.signVariationsLeft_sub_signVariationsRight {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) : ↑(signVariationsLeft (p :: cs) a) - ↑(signVariationsRight (p :: cs) a) = if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0

The contribution of a point. For a signed remainder chain with head p and query seed f, the variations drop across a by the sign of f at a if a is a root of p, and do not change otherwise.

theorem TauCeti.Sturm.sum_sign_Ioc {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) : (↑(signVariationsRight (p :: cs) a) - ↑(signVariationsLeft (p :: cs) b) + if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) = ∑ r ∈ p.roots.toFinset with a < r ∧ r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on (a, b]. The contribution of the closed endpoint b is added explicitly to the open-interval formula.

theorem TauCeti.Sturm.sum_sign_Ico {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) : (↑(signVariationsRight (p :: cs) a) - ↑(signVariationsLeft (p :: cs) b) + if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) = ∑ r ∈ p.roots.toFinset with a ≤ r ∧ r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on [a, b). The contribution of the closed endpoint a is added explicitly to the open-interval formula.

theorem TauCeti.Sturm.sum_sign_Icc {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) : ((↑(signVariationsRight (p :: cs) a) - ↑(signVariationsLeft (p :: cs) b) + if Polynomial.eval a p = 0 then ↑(SignType.sign (Polynomial.eval a f)) else 0) + if Polynomial.eval b p = 0 then ↑(SignType.sign (Polynomial.eval b f)) else 0) = ∑ r ∈ p.roots.toFinset with a ≤ r ∧ r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on [a, b]. The contributions of both closed endpoints are added explicitly to the open-interval formula. For a = b this is the contribution of a point.

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

One-sided Sturm–Tarski on (a, b) for Mathlib's signed remainder sequence.

theorem TauCeti.Sturm.sum_sign_sturmSeq_Ioc {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a b : R} {p : Polynomial R} (hp : p ≠ 0) (f : Polynomial R) (hab : a ≤ b) : (↑(signVariationsRight (p.sturmSeq (f * Polynomial.derivative p)) a) - ↑(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 a < r ∧ r ≤ b, ↑(SignType.sign (Polynomial.eval r f))

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

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

One-sided Sturm–Tarski on [a, b) for Mathlib's signed remainder sequence.

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

One-sided Sturm–Tarski on [a, b] for Mathlib's signed remainder sequence.

theorem TauCeti.Sturm.card_roots_toFinset_Ioo {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a b : R} (p : Polynomial R) (hab : a < b) : ↑(signVariationsRight (p.sturmSeq (Polynomial.derivative p)) a) - ↑(signVariationsLeft (p.sturmSeq (Polynomial.derivative p)) b) = ↑{r ∈ p.roots.toFinset | a < r ∧ r < b}.card

Sturm's count of the distinct roots in (a, b), with no condition on the endpoints.

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

Sturm's count of the distinct roots in (a, b].

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

Sturm's count of the distinct roots in [a, b).

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

Sturm's count of the distinct roots in [a, b].