Sturm–Tarski with infinite endpoints

Leading coefficients and degree parity compute the sign variations at both infinities. Together with one-sided signs at finite endpoints, these give half-line and whole-field Sturm–Tarski identities for signed remainder chains and for Polynomial.sturmSeq, including root counts. Finite endpoints may be roots of any chain entry.

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

Sign variations at positive infinity.

Equations

• TauCeti.Sturm.signVariationsAtTop cs = (List.map Polynomial.leadingCoeff cs).signVariations

theorem TauCeti.Sturm.signVariationsAtTop_def {R : Type u_1} [Semiring R] [LinearOrder R] (cs : List (Polynomial R)) : signVariationsAtTop cs = (List.map Polynomial.leadingCoeff cs).signVariations

Unfold positive-infinity variations as variations of the leading coefficients.

@[simp]

theorem TauCeti.Sturm.signVariationsAtTop_nil {R : Type u_1} [Semiring R] [LinearOrder R] : signVariationsAtTop [] = 0

@[simp]

theorem TauCeti.Sturm.signVariationsAtTop_singleton {R : Type u_1} [Semiring R] [LinearOrder R] (p : Polynomial R) : signVariationsAtTop [p] = 0

theorem TauCeti.Sturm.signVariationsAt_eq_atTop {R : Type u_1} [Semiring R] [LinearOrder R] {cs : List (Polynomial R)} {x : R} (h : ∀ p ∈ cs, SignType.sign (Polynomial.eval x p) = SignType.sign p.leadingCoeff) : signVariationsAt cs x = signVariationsAtTop cs

Matching the leading-coefficient signs realizes positive-infinity variations.

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

Sign variations at negative infinity.

Equations

• TauCeti.Sturm.signVariationsAtBot cs = (List.map (fun (p : Polynomial R) => p.leadingCoeff * (-1) ^ p.natDegree) cs).signVariations

theorem TauCeti.Sturm.signVariationsAtBot_def {R : Type u_1} [Ring R] [LinearOrder R] (cs : List (Polynomial R)) : signVariationsAtBot cs = (List.map (fun (p : Polynomial R) => p.leadingCoeff * (-1) ^ p.natDegree) cs).signVariations

Unfold negative-infinity variations using leading coefficients and degree parity.

@[simp]

theorem TauCeti.Sturm.signVariationsAtBot_nil {R : Type u_1} [Ring R] [LinearOrder R] : signVariationsAtBot [] = 0

@[simp]

theorem TauCeti.Sturm.signVariationsAtBot_singleton {R : Type u_1} [Ring R] [LinearOrder R] (p : Polynomial R) : signVariationsAtBot [p] = 0

theorem TauCeti.Sturm.signVariationsAt_eq_atBot {R : Type u_1} [Ring R] [LinearOrder R] {cs : List (Polynomial R)} {x : R} (h : ∀ p ∈ cs, SignType.sign (Polynomial.eval x p) = SignType.sign (p.leadingCoeff * (-1) ^ p.natDegree)) : signVariationsAt cs x = signVariationsAtBot cs

Matching the parity-adjusted leading signs realizes negative-infinity variations.

theorem TauCeti.Sturm.exists_signVariationsAtTop {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) : ∃ (B : R), ∀ (x : R), B < x → signVariationsAt cs x = signVariationsAtTop cs

The variation count stabilizes at positive infinity, even for lists containing zero.

theorem TauCeti.Sturm.exists_signVariationsAtBot {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) : ∃ (B : R), ∀ x < B, signVariationsAt cs x = signVariationsAtBot cs

The variation count stabilizes at negative infinity, even for lists containing zero.

theorem TauCeti.Sturm.exists_atTop {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (hne : ∀ p ∈ cs, p ≠ 0) : ∃ (B : R), (∀ (x : R), B < x → signVariationsAt cs x = signVariationsAtTop cs) ∧ ∀ p ∈ cs, ∀ (r : R), Polynomial.eval r p = 0 → r ≤ B

Far enough to the right, finite evaluation realizes the infinity signs and lies beyond every chain root. The bound belongs to the ordered field itself.

theorem TauCeti.Sturm.exists_atBot {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] (cs : List (Polynomial R)) (hne : ∀ p ∈ cs, p ≠ 0) : ∃ (B : R), (∀ x < B, signVariationsAt cs x = signVariationsAtBot cs) ∧ ∀ p ∈ cs, ∀ (r : R), Polynomial.eval r p = 0 → B ≤ r

Far enough to the left, finite evaluation realizes the negative-infinity variations, and every chain root lies above the bound.

theorem TauCeti.Sturm.sum_sign_Ioi {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)) = ∑ r ∈ p.roots.toFinset with a < r, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on (a, ∞), using right-hand variations at any finite endpoint.

theorem TauCeti.Sturm.sum_sign_Iio {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) = ∑ r ∈ p.roots.toFinset with r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on (-∞, b), using left-hand variations at any finite endpoint.

theorem TauCeti.Sturm.sum_sign_univ {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)) : ↑(signVariationsAtBot (p :: cs)) - ↑(signVariationsAtTop (p :: cs)) = ∑ r ∈ p.roots.toFinset, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski on the whole real closed field.

theorem TauCeti.Sturm.sum_sign_sturmSeq_Ioi {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))) = ∑ r ∈ p.roots.toFinset with a < r, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for Mathlib's sequence on (a, ∞), even when a is a root.

theorem TauCeti.Sturm.sum_sign_sturmSeq_Iio {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) = ∑ r ∈ p.roots.toFinset with r < b, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for Mathlib's sequence on (-∞, b), even when b is a root.

theorem TauCeti.Sturm.sum_sign_sturmSeq_univ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p f : Polynomial R) : ↑(signVariationsAtBot (p.sturmSeq (f * Polynomial.derivative p))) - ↑(signVariationsAtTop (p.sturmSeq (f * Polynomial.derivative p))) = ∑ r ∈ p.roots.toFinset, ↑(SignType.sign (Polynomial.eval r f))

Sturm–Tarski for Mathlib's signed remainder sequence on the whole real closed field.

theorem TauCeti.Sturm.card_roots_toFinset_Ioi {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))) = ↑{x ∈ p.roots.toFinset | a < x}.card

Sturm counting of distinct roots in (a, ∞), with no restriction on the endpoint.

theorem TauCeti.Sturm.card_roots_toFinset_Iio {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) = ↑{x ∈ p.roots.toFinset | x < b}.card

Sturm counting of distinct roots in (-∞, b), with no restriction on the endpoint.

theorem TauCeti.Sturm.card_roots_toFinset_univ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] (p : Polynomial R) : ↑(signVariationsAtBot (p.sturmSeq (Polynomial.derivative p))) - ↑(signVariationsAtTop (p.sturmSeq (Polynomial.derivative p))) = ↑p.roots.toFinset.card

Classical Sturm counting of all distinct roots of a nonzero polynomial. For p = 0 both sides are zero: sturmSeq 0 _ = [] and Polynomial.roots 0 = 0 by convention.