What Sturm's theorem says about an interval

The consequences of Sturm's theorem (Ratpoints.SturmTheorem) for an interval with ends that may be infinite, which the bisection of the Sturm step relies on: the counts of the Sturm sequence at the ends (Ratpoints.vLeft, Ratpoints.vRight: V(l) at the lower end, V(r) plus 1 at a root r at the upper end, V(∓∞) at the ends at infinity) agree exactly when the squarefree polynomial F has no root strictly between them (Ratpoints.vLeft_eq_vRight_iff); then, when F is negative just inside the lower end, it is negative between the ends and just inside the upper end (Ratpoints.eval_neg_of_vLeft_eq_vRight); when the counts differ, or F is positive just inside the lower end, F is positive somewhere between the ends (Ratpoints.exists_inside_eval_pos); and equal counts at ∓∞ leave no root at all, so that F is negative everywhere when it is negative at 0 (Ratpoints.eval_neg_of_vBot_eq_vTop). Infinite ends are replaced by points far out, where the counts and the signs are those at infinity (Ratpoints.eventually_atBot_sturm, Ratpoints.eventually_atTop_sturm).

Main definitions

• Ratpoints.sturmV, Ratpoints.vBot, Ratpoints.vTop: the counts of the Sturm sequence at a point and at ∓∞.
• Ratpoints.vLeft, Ratpoints.vRight, Ratpoints.sgnLeftEnd, Ratpoints.sgnRightEnd: the counts at the ends of an interval and, for a squarefree F, the signs of F just inside them.
• Ratpoints.Inside: a point strictly between the ends.

Main statements

• Ratpoints.sturmV_eq_iff: the counts at finite ends agree exactly when no root lies between.
• Ratpoints.vLeft_eq_vRight_iff: the same for ends that may be infinite.
• Ratpoints.eval_neg_of_vLeft_eq_vRight: an interval that the bisection drops holds no x with F(x) ≥ 0.
• Ratpoints.exists_inside_eval_pos: an interval that the bisection keeps holds an x with F(x) > 0.
• Ratpoints.eval_neg_of_vBot_eq_vTop: a polynomial with equal counts at ∓∞, negative at 0, is negative everywhere.

@[reducible, inline]

noncomputable abbrev Ratpoints.sturmV (F : Polynomial ℝ) (x : ℝ) : ℕ

The number of sign variations of the Sturm sequence of F and F' at x, the count of Ratpoints.SturmTheorem.

Equations

• Ratpoints.sturmV F x = (List.map (Polynomial.eval x) (F.sturmSeq (Polynomial.derivative F))).signVariations

noncomputable def Ratpoints.vBot (F : Polynomial ℝ) : ℕ

The count of the Sturm sequence of F and F' at -∞: the number of sign variations of the leading coefficients of its entries, each times (-1) ^ deg.

Equations

• Ratpoints.vBot F = (List.map (fun (p : Polynomial ℝ) => (-1) ^ p.natDegree * p.leadingCoeff) (F.sturmSeq (Polynomial.derivative F))).signVariations

noncomputable def Ratpoints.vTop (F : Polynomial ℝ) : ℕ

The count of the Sturm sequence of F and F' at +∞: the number of sign variations of the leading coefficients of its entries.

Equations

• Ratpoints.vTop F = (List.map Polynomial.leadingCoeff (F.sturmSeq (Polynomial.derivative F))).signVariations

noncomputable def Ratpoints.vLeft (F : Polynomial ℝ) : Option ℝ → ℕ

The count at the lower end l of an interval, none for -∞: V(l), or V(-∞).

Equations

• Ratpoints.vLeft F none = Ratpoints.vBot F
• Ratpoints.vLeft F (some a) = Ratpoints.sturmV F a

noncomputable def Ratpoints.vRight (F : Polynomial ℝ) : Option ℝ → ℕ

The count at the upper end r of an interval, none for +∞: V(r), plus 1 at a root of F, or V(+∞).

Equations

• Ratpoints.vRight F none = Ratpoints.vTop F
• Ratpoints.vRight F (some a) = Ratpoints.sturmV F a + if F.IsRoot a then 1 else 0

noncomputable def Ratpoints.sgnLeftEnd (F : Polynomial ℝ) : Option ℝ → SignType

At the lower end l of an interval, none for -∞: the sign of (-1) ^ deg F times the leading coefficient of F at -∞, and at a finite end a that of F(a), or of F'(a) when F(a) = 0. This is the sign of F just inside the end when F(a) and F'(a) do not both vanish, as for a squarefree F, where it is not zero (Ratpoints.sgnLeftEnd_ne_zero).

Equations

• Ratpoints.sgnLeftEnd F none = SignType.sign ((-1) ^ F.natDegree * F.leadingCoeff)
• Ratpoints.sgnLeftEnd F (some a) = if Polynomial.eval a F = 0 then SignType.sign (Polynomial.eval a (Polynomial.derivative F)) else SignType.sign (Polynomial.eval a F)

noncomputable def Ratpoints.sgnRightEnd (F : Polynomial ℝ) : Option ℝ → SignType

At the upper end r of an interval, none for +∞: the sign of the leading coefficient of F at +∞, and at a finite end b that of F(b), or of -F'(b) when F(b) = 0. This is the sign of F just inside the end when F(b) and F'(b) do not both vanish, as for a squarefree F.

Equations

• Ratpoints.sgnRightEnd F none = SignType.sign F.leadingCoeff
• Ratpoints.sgnRightEnd F (some a) = if Polynomial.eval a F = 0 then -SignType.sign (Polynomial.eval a (Polynomial.derivative F)) else SignType.sign (Polynomial.eval a F)

def Ratpoints.Inside (l r : Option ℝ) (x : ℝ) : Prop

x lies strictly between the ends l and r, none for ∓∞.

Equations

• Ratpoints.Inside l r x = ((∀ a ∈ l, a < x) ∧ ∀ b ∈ r, x < b)

theorem Ratpoints.sturmV_eq_iff (hS : SturmTheorem) {F : Polynomial ℝ} (hF : Squarefree F) {l r : ℝ} (hlr : l < r) : (sturmV F l = sturmV F r + if F.IsRoot r then 1 else 0) ↔ ∀ (x : ℝ), l < x → x < r → ¬F.IsRoot x

By Sturm's theorem, the counts V(l) and V(r), plus 1 at a root r, agree exactly when F has no root in (l, r), for l < r.

theorem Ratpoints.eventually_atBot_sturm {F : Polynomial ℝ} (hF : F ≠ 0) : ∀ᶠ (y : ℝ) in Filter.atBot, sturmV F y = vBot F ∧ ¬F.IsRoot y ∧ SignType.sign (Polynomial.eval y F) = SignType.sign ((-1) ^ F.natDegree * F.leadingCoeff)

Far left, the count is V(-∞), F has no root, and the sign of F is that at -∞.

theorem Ratpoints.eventually_atTop_sturm {F : Polynomial ℝ} (hF : F ≠ 0) : ∀ᶠ (y : ℝ) in Filter.atTop, sturmV F y = vTop F ∧ ¬F.IsRoot y ∧ SignType.sign (Polynomial.eval y F) = SignType.sign F.leadingCoeff

Far right, the count is V(+∞), F has no root, and the sign of F is that of its leading coefficient.

theorem Ratpoints.exists_lt_sturmV_eq_vLeft {F : Polynomial ℝ} (hF : F ≠ 0) {l : Option ℝ} {x : ℝ} (hx : ∀ a ∈ l, a < x) : ∃ l' < x, (∀ a ∈ l, l' = a) ∧ sturmV F l' = vLeft F l ∧ sgnLeftEnd F (some l') = sgnLeftEnd F l

A finite point l' < x standing for the lower end l left of x: l itself, or a point far left, with the count and the sign just right of it of the end.

theorem Ratpoints.exists_gt_sturmV_add_eq_vRight {F : Polynomial ℝ} (hF : F ≠ 0) {r : Option ℝ} {x : ℝ} (hx : ∀ b ∈ r, x < b) : ∃ r' > x, (∀ b ∈ r, r' = b) ∧ (sturmV F r' + if F.IsRoot r' then 1 else 0) = vRight F r ∧ sgnRightEnd F (some r') = sgnRightEnd F r

A finite point r' > x standing for the upper end r right of x: r itself, or a point far right, with the count and the sign just left of it of the end.

theorem Ratpoints.exists_inside {l r : Option ℝ} (hlr : ∀ a ∈ l, ∀ b ∈ r, a < b) : ∃ (x : ℝ), Inside l r x

Ends in order have a point between them.

theorem Ratpoints.eventually_inside {l r : Option ℝ} {x : ℝ} (hx : Inside l r x) : ∀ᶠ (y : ℝ) in nhds x, Inside l r y

Near a point between the ends, every point lies between them.

theorem Ratpoints.vLeft_eq_vRight_iff (hS : SturmTheorem) {F : Polynomial ℝ} (hF : Squarefree F) {l r : Option ℝ} (hlr : ∀ a ∈ l, ∀ b ∈ r, a < b) : vLeft F l = vRight F r ↔ ∀ (x : ℝ), Inside l r x → ¬F.IsRoot x

By Sturm's theorem, the counts at the ends of an interval agree exactly when F has no root strictly between them.

theorem Ratpoints.sgnLeftEnd_ne_zero {F : Polynomial ℝ} (hF : Squarefree F) (l : Option ℝ) : sgnLeftEnd F l ≠ 0

The sign of a squarefree F just inside a lower end is not zero.

theorem Ratpoints.eval_neg_of_vLeft_eq_vRight (hS : SturmTheorem) {F : Polynomial ℝ} (hF : Squarefree F) {l r : Option ℝ} (hlr : ∀ a ∈ l, ∀ b ∈ r, a < b) (h : vLeft F l = vRight F r) (hs : sgnLeftEnd F l = -1) : (∀ (x : ℝ), Inside l r x → Polynomial.eval x F < 0) ∧ sgnRightEnd F r = -1

By Sturm's theorem, when the counts at the ends of an interval agree and F is negative just inside its lower end, F is negative between the ends and just inside the upper end: the interval holds no x with F(x) ≥ 0.

theorem Ratpoints.eval_neg_of_vBot_eq_vTop (hS : SturmTheorem) {F : Polynomial ℝ} (hF : Squarefree F) (h : vBot F = vTop F) (h0 : Polynomial.eval 0 F < 0) (x : ℝ) : Polynomial.eval x F < 0

By Sturm's theorem, a squarefree real polynomial with equal counts at ∓∞ has no real root, so that it is negative everywhere when it is negative at 0.

theorem Ratpoints.exists_inside_eval_pos_of_isRoot {F : Polynomial ℝ} (hF : Squarefree F) {l r : Option ℝ} {z : ℝ} (hz : Inside l r z) (hz0 : F.IsRoot z) : ∃ (x : ℝ), Inside l r x ∧ 0 < Polynomial.eval x F

Next to a root of a squarefree F between the ends of an interval, F is positive at some point between them: it changes its sign at the root.

theorem Ratpoints.exists_inside_eval_pos (hS : SturmTheorem) {F : Polynomial ℝ} (hF : Squarefree F) {l r : Option ℝ} (hlr : ∀ a ∈ l, ∀ b ∈ r, a < b) (h : vLeft F l ≠ vRight F r ∨ sgnLeftEnd F l = 1) : ∃ (x : ℝ), Inside l r x ∧ 0 < Polynomial.eval x F

By Sturm's theorem, F is positive at some point between the ends of an interval when the counts at its ends differ, so that a root lies between them, or when F is positive just inside its lower end.