noncomputable def Sturm.sturmVar (chain : List (Polynomial ℝ)) (x : ℝ) : ℕ

Zero-skipping sign variations of the chain chain evaluated at x: the sign variations of the list of evaluations chain.map (·.eval x).

Equations

• Sturm.sturmVar chain x = (List.map (Polynomial.eval x) chain).signVariations

@[simp]

theorem Sturm.sturmVar_nil (x : ℝ) : sturmVar [] x = 0

theorem Sturm.sturmVar_cons_zero {q : Polynomial ℝ} {x : ℝ} (h : Polynomial.eval x q = 0) (chain : List (Polynomial ℝ)) : sturmVar (q :: chain) x = sturmVar chain x

A chain element that vanishes at x contributes no variation at x: sturmVar ignores it.

noncomputable def Sturm.firstSign (l : List ℝ) : SignType

The sign of the first nonzero entry of a real list, or 0 if every entry is zero.

Equations

• Sturm.firstSign l = (Option.map (⇑SignType.sign) (List.filter (fun (v : ℝ) => decide (v ≠ 0)) l).head?).getD 0

@[simp]

theorem Sturm.firstSign_nil : firstSign [] = 0

@[simp]

theorem Sturm.firstSign_cons_zero (l : List ℝ) : firstSign (0 :: l) = firstSign l

@[simp]

theorem Sturm.firstSign_cons_ne {a : ℝ} (l : List ℝ) (ha : a ≠ 0) : firstSign (a :: l) = SignType.sign a

theorem Sturm.signVariations_cons {a : ℝ} (l : List ℝ) (ha : a ≠ 0) : (a :: l).signVariations = (if SignType.sign a * firstSign l = -1 then 1 else 0) + l.signVariations

Prepending a nonzero entry a adds one variation exactly when its sign is opposite the sign of the next surviving entry.

noncomputable def Sturm.sturmVarPosInf (chain : List (Polynomial ℝ)) : ℕ

Sign variations of the chain at +∞: the sign of each element there is the sign of its leading coefficient, so this is the zero-skipping variation count of the leading coefficients. The zero polynomial contributes leading coefficient 0, which the zero-skipping convention drops.

Equations

• Sturm.sturmVarPosInf chain = (List.map Polynomial.leadingCoeff chain).signVariations

noncomputable def Sturm.sturmVarNegInf (chain : List (Polynomial ℝ)) : ℕ

Sign variations of the chain at −∞: the sign of an element there is the sign of its leading coefficient times (-1) ^ degree, so this is the zero-skipping variation count of leadingCoeff · (-1) ^ natDegree.

Equations

• Sturm.sturmVarNegInf chain = (List.map (fun (q : Polynomial ℝ) => q.leadingCoeff * (-1) ^ q.natDegree) chain).signVariations

structure Sturm.IsSturmChain (p : Polynomial ℝ) (chain : List (Polynomial ℝ)) : Prop

A generalized Sturm chain for a real polynomial.

At a root of the first polynomial, the product of the first two entries changes from negative to positive. At a root of an interior entry, its neighbors have opposite signs. The last entry has no real roots, and every entry is nonzero.

These conditions allow the one-element chain of a nonzero constant polynomial.

• head : chain.head? = some p

  The head of the chain is p.

• root_flank (r : ℝ) : p.IsRoot r → ∃ (q : Polynomial ℝ), chain[1]? = some q ∧ Polynomial.eval r q ≠ 0 ∧ (∀ᶠ (x : ℝ) in nhdsWithin r (Set.Iio r), Polynomial.eval x (p * q) < 0) ∧ ∀ᶠ (x : ℝ) in nhdsWithin r (Set.Ioi r), 0 < Polynomial.eval x (p * q)

  At every real root r of p, the chain has a second element q, nonzero at r, with p * q negative just left of r and positive just right of r.

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

  No chain element is the zero polynomial.

• 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

  Whenever the interior element b = chain[i+1] vanishes at x, its two neighbours a = chain[i] and c = chain[i+2] are nonzero there and have opposite signs.

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

  The last element of the chain has no real zero.

theorem Sturm.IsSturmChain.nonempty {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (h : IsSturmChain p chain) : chain ≠ []

A Sturm chain is nonempty.

theorem Sturm.IsSturmChain.head_mem {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (h : IsSturmChain p chain) : p ∈ chain

The polynomial counted by a Sturm chain is its first entry.

theorem Sturm.IsSturmChain.ne_zero {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (h : IsSturmChain p chain) : p ≠ 0

A polynomial admitting a Sturm chain is nonzero.