theorem Sturm.sturmVar_const_of_no_zero {chain : List (Polynomial ℝ)} (a b : ℝ) (hab : a ≤ b) (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, Polynomial.eval x q ≠ 0) : sturmVar chain a = sturmVar chain b

Sign variations are constant on an interval containing no zero of any chain entry.

theorem Sturm.sturmVar_interior_cross {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (hchain : IsSturmChain p chain) (r : ℝ) (hpr : ¬p.IsRoot r) (a b : ℝ) (har : a < r) (hrb : r < b) (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, x ≠ r → Polynomial.eval x q ≠ 0) : sturmVar chain a = sturmVar chain r ∧ sturmVar chain r = sturmVar chain b

Crossing a zero of an interior entry preserves the variation count.

theorem Sturm.sturmVar_root_cross {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (hchain : IsSturmChain p chain) (r : ℝ) (hr : p.IsRoot r) (a b : ℝ) (har : a < r) (hrb : r < b) (hz : ∀ q ∈ chain, ∀ x ∈ Set.Icc a b, x ≠ r → Polynomial.eval x q ≠ 0) : sturmVar chain a = sturmVar chain b + 1 ∧ sturmVar chain r = sturmVar chain b

Crossing a root of the first entry decreases the variation count by one. The count at the root equals the count just to its right.

noncomputable def Sturm.chainZeros (cs : List (Polynomial ℝ)) : Finset ℝ

The union of the real root sets of the chain entries.

Equations

• Sturm.chainZeros cs = cs.toFinset.biUnion fun (q : Polynomial ℝ) => q.roots.toFinset

theorem Sturm.mem_chainZeros {cs : List (Polynomial ℝ)} (hne : ∀ q ∈ cs, q ≠ 0) {x : ℝ} : x ∈ chainZeros cs ↔ ∃ q ∈ cs, Polynomial.eval x q = 0

Membership in chainZeros: a point lies in it exactly when some chain element vanishes there (using that every chain element is nonzero).

theorem Sturm.sturmVar_eq_right {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (hchain : IsSturmChain p chain) {z c : ℝ} (hzc : z ≤ c) (hclear : ∀ (x : ℝ), z < x → x ≤ c → x ∉ chainZeros chain) : sturmVar chain z = sturmVar chain c

The variation count agrees with its value immediately to the right, including at zeros of chain entries.

theorem Sturm.IsSturmChain.sturm_Ioc {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (hchain : IsSturmChain p chain) (hnod : p.roots.Nodup) {a b : ℝ} (hab : a ≤ b) : sturmVar chain b + (Multiset.filter (fun (r : ℝ) => r ∈ Set.Ioc a b) p.roots).card = sturmVar chain a

Sturm's theorem on a half-open interval.

The decrease in sign variations from a to b counts the roots in (a, b]. The hypothesis on p.roots ensures each real root has multiplicity one.

theorem Sturm.eval_sign_pos_inf {q : Polynomial ℝ} (hq : q ≠ 0) {x : ℝ} (hbeyond : ∀ (y : ℝ), q.IsRoot y → y < x) : SignType.sign (Polynomial.eval x q) = SignType.sign q.leadingCoeff

Sign at +∞. Past all its real roots, a nonzero real polynomial has the sign of its leading coefficient.

theorem Sturm.eval_sign_neg_inf {q : Polynomial ℝ} (hq : q ≠ 0) {x : ℝ} (hbeyond : ∀ (y : ℝ), q.IsRoot y → x < y) : SignType.sign (Polynomial.eval x q) = SignType.sign (q.leadingCoeff * (-1) ^ q.natDegree)

Sign at −∞. Below all its real roots, a nonzero real polynomial has the sign of leadingCoeff · (-1) ^ natDegree.

theorem Sturm.IsSturmChain.sturm {p : Polynomial ℝ} {chain : List (Polynomial ℝ)} (hchain : IsSturmChain p chain) (hnod : p.roots.Nodup) : sturmVarPosInf chain + p.roots.card = sturmVarNegInf chain

Sturm's theorem on the real line: the decrease in sign variations from -∞ to +∞ counts all real roots.