structure Sturm.RemainderChain (chain : List (Polynomial ℝ)) : Prop

The algebraic conditions on a signed remainder chain, before checking its seeds.

• nonzero_mem (p : Polynomial ℝ) : p ∈ chain → p ≠ 0

  Every entry is a nonzero polynomial.

• coprime (i : ℕ) (a b : Polynomial ℝ) : chain[i]? = some a → chain[i + 1]? = some b → IsCoprime a b

  Consecutive entries are coprime.

• interior_alternates (i : ℕ) (x : ℝ) (a b c : Polynomial ℝ) : chain[i]? = some a → chain[i + 1]? = some b → chain[i + 2]? = some c → Polynomial.eval x b = 0 → Polynomial.eval x a ≠ 0 ∧ Polynomial.eval x c ≠ 0 ∧ Polynomial.eval x a * Polynomial.eval x c < 0

  Neighbors of a vanishing interior entry have opposite signs.

• last_no_root (p : Polynomial ℝ) : chain.getLast? = some p → ∀ (x : ℝ), Polynomial.eval x p ≠ 0

  The last entry has no real roots.

theorem Sturm.RemainderChain.pair {p : Polynomial ℝ} {c : ℝ} (hp : p ≠ 0) (hc : c ≠ 0) : RemainderChain [p, Polynomial.C c]

Terminate a certificate at a nonzero constant.

theorem Sturm.RemainderChain.cons {p q r : Polynomial ℝ} {tail : List (Polynomial ℝ)} {a b : ℝ} {d : Polynomial ℝ} (h : RemainderChain (q :: r :: tail)) (hp : p ≠ 0) (ha : 0 < a) (hb : 0 < b) (hid : Polynomial.C a * p = d * q - Polynomial.C b * r) : RemainderChain (p :: q :: r :: tail)

Prepend a positive multiple of a signed remainder identity.

theorem Sturm.RemainderChain.isSturmChain {p q : Polynomial ℝ} {tail : List (Polynomial ℝ)} {a : ℝ} (h : RemainderChain (p :: q :: tail)) (ha : 0 < a) (hd : Polynomial.derivative p = Polynomial.C a * q) : IsSturmChain p (p :: q :: tail)

A remainder chain starting with a positive multiple of the derivative is a Sturm chain.

theorem Sturm.RemainderChain.separable {p q : Polynomial ℝ} {tail : List (Polynomial ℝ)} {a : ℝ} (h : RemainderChain (p :: q :: tail)) (ha : a ≠ 0) (hd : Polynomial.derivative p = Polynomial.C a * q) : p.Separable

A remainder chain whose second entry is a nonzero multiple of the derivative certifies separability.

theorem Sturm.RemainderChain.card_rootSet {R : Type u_1} [CommRing R] [Algebra R ℝ] {f : Polynomial R} {p q : Polynomial ℝ} {tail : List (Polynomial ℝ)} {a : ℝ} {n : ℕ} (h : RemainderChain (p :: q :: tail)) (ha : 0 < a) (hd : Polynomial.derivative p = Polynomial.C a * q) (hf : Polynomial.map (algebraMap R ℝ) f = p) (hn : sturmVarPosInf (p :: q :: tail) + n = sturmVarNegInf (p :: q :: tail)) : Fintype.card ↑(f.rootSet ℝ) = n

Convert the variation count of a checked chain to the number of distinct real roots.