noncomputable def Sturm.countSignChanges : List ℝ → ℕ

Count the sign changes of a real list: the number of adjacent pairs whose product is negative. Callers first drop the zero entries (see Sturm.signVariations), so on a zero-free list this is exactly the number of adjacent opposite-sign pairs.

Equations

• Sturm.countSignChanges (a :: b :: rest) = (if a * b < 0 then 1 else 0) + Sturm.countSignChanges (b :: rest)
• Sturm.countSignChanges x✝ = 0

@[simp]

theorem Sturm.countSignChanges_nil : countSignChanges [] = 0

@[simp]

theorem Sturm.countSignChanges_singleton (a : ℝ) : countSignChanges [a] = 0

theorem Sturm.countSignChanges_cons_cons (a b : ℝ) (rest : List ℝ) : countSignChanges (a :: b :: rest) = (if a * b < 0 then 1 else 0) + countSignChanges (b :: rest)

noncomputable def Sturm.signVariations (l : List ℝ) : ℕ

Zero-skipping sign variations of a real list: drop the zeros, then count the adjacent opposite-sign pairs. This is the variation count that both the pointwise chain evaluations and the leading-coefficient signs at ±∞ feed into.

Equations

• Sturm.signVariations l = Sturm.countSignChanges (List.filter (fun (v : ℝ) => decide (v ≠ 0)) l)

@[simp]

theorem Sturm.signVariations_nil : signVariations [] = 0

@[simp]

theorem Sturm.signVariations_singleton (a : ℝ) : signVariations [a] = 0

@[simp]

theorem Sturm.signVariations_cons_zero (l : List ℝ) : signVariations (0 :: l) = signVariations l

Prepending a zero entry does not change the sign variations.

theorem Sturm.signVariations_cons_ne (a : ℝ) (l : List ℝ) (ha : a ≠ 0) : signVariations (a :: l) = countSignChanges (a :: List.filter (fun (v : ℝ) => decide (v ≠ 0)) l)

A nonzero first entry survives removal of zero entries.

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 = Sturm.signVariations (List.map (Polynomial.eval x) chain)

@[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.

theorem Sturm.countSignChanges_congr {l₁ l₂ : List ℝ} (h : List.Forall₂ (fun (u v : ℝ) => SignType.sign u = SignType.sign v) l₁ l₂) : countSignChanges l₁ = countSignChanges l₂

Two real lists whose entries have pointwise equal signs have equal countSignChanges: the sign-change count reads only the signs of the entries.

theorem Sturm.signVariations_congr {l₁ l₂ : List ℝ} (h : List.Forall₂ (fun (u v : ℝ) => SignType.sign u = SignType.sign v) l₁ l₂) : signVariations l₁ = signVariations l₂

signVariations reads only the signs of the entries: two real lists whose entries are pointwise sign-equal have equal sign variations.

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) : signVariations (a :: l) = (if SignType.sign a * firstSign l = -1 then 1 else 0) + signVariations l

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 = Sturm.signVariations (List.map Polynomial.leadingCoeff chain)

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 = Sturm.signVariations (List.map (fun (q : Polynomial ℝ) => q.leadingCoeff * (-1) ^ q.natDegree) chain)

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.