The signs of the chain of the Sturm step

The signs that the Sturm step computes, in the terms of Mathlib: the Horner value of Ratpoints.Sturm.evalSign is 2 ^ (e deg) times the value of the polynomial of the row at n / 2 ^ e (Ratpoints.Sturm.hornerValue_eq_eval), so that Ratpoints.Sturm.evalSign computes its sign (Ratpoints.Sturm.run_evalSign_eq_sign_eval); the count of Ratpoints.Sturm.signsAt at a point where f and f' do not both vanish is the number of sign variations (List.signVariations) of the signs of the rows there (Ratpoints.Sturm.run_signsAt_eq_signVariations); and the counts of Ratpoints.Sturm.countsAtInfinity are the numbers of sign variations of the signs of the leading coefficients, negated for odd degree at -∞ (Ratpoints.Sturm.run_countsAtInfinity_eq_signVariations).

The rows of a chain whose last row is constant are, over ℚ, positive multiples of the entries of Mathlib's Polynomial.sturmSeq of f and f' (Ratpoints.Sturm.IsChain.forall₂_posAssoc_sturmSeq, from Ratpoints.Sturm.IsChain.exists_mul_eq), and so over ℝ (Ratpoints.Sturm.IsChain.forall₂_posAssoc_sturmSeq_map); hence, for a polynomial of degree d < 2 ^ 57 and the depths up to 55 of the Sturm step, Ratpoints.Sturm.signsAt computes the signs of the real polynomial f and its derivative and the count V of Sturm's theorem (Ratpoints.Sturm.IsChain.run_signsAt_eq), and Ratpoints.Sturm.countsAtInfinity the counts V(+∞) and V(-∞) (Ratpoints.Sturm.IsChain.run_countsAtInfinity_eq).

Main definitions

• Ratpoints.Sturm.rowPolys: the polynomials over ℚ of the rows of a chain.
• Ratpoints.Sturm.chainPoly: the real polynomial of a chain.

Main statements

• Ratpoints.Sturm.hornerValue_eq_eval, Ratpoints.Sturm.run_evalSign_eq_sign_eval: the value and the sign of a row at a dyadic number.
• Ratpoints.Sturm.signCount_eq_signVariations, Ratpoints.Sturm.ite_add_signCount_eq_signVariations, Ratpoints.Sturm.run_signsAt_eq_signVariations: the count of the signs at a midpoint.
• Ratpoints.Sturm.run_countsAtInfinity_eq_signVariations: the counts at ±∞.
• Ratpoints.Sturm.IsChain.forall₂_posAssoc_sturmSeq_map: the chain as the Sturm sequence over ℝ.
• Ratpoints.Sturm.IsChain.run_signsAt_eq, Ratpoints.Sturm.IsChain.run_countsAtInfinity_eq: the signs and counts of the Sturm step are those of the real polynomial.

theorem Ratpoints.Sturm.hornerValue_eq_sum (row : Array ℤ) (n : ℤ) (e j : ℕ) : hornerValue row n e j = ∑ i ∈ Finset.range (j + 1), row[row.size - 1 - i]! * n ^ (j - i) * 2 ^ (e * i)

The Horner value after j steps, ∑ c_(deg - i) n ^ (j - i) 2 ^ (e i) over i ≤ j.

theorem Ratpoints.Sturm.hornerValue_eq_eval (row : Array ℤ) (n : ℤ) (e : ℕ) (h : row.size ≠ 0) : ↑(hornerValue row n e (row.size - 1)) = 2 ^ (e * (row.size - 1)) * Polynomial.eval (↑n / 2 ^ e) (poly row.toList)

The Horner value of Ratpoints.Sturm.evalSign is 2 ^ (e deg) times the value of the polynomial of the row at n / 2 ^ e.

theorem Ratpoints.Sturm.run_evalSign_eq_sign_eval {row : Array ℤ} (h : row.size ≠ 0) (num : Int64) {denexp : Int64} (h0 : 0 ≤ denexp.toInt) (hd : denexp.toInt * ↑row.size < 2 ^ 63) : (evalSign row num denexp).run = ↑(SignType.sign (Polynomial.eval (↑num.toInt / 2 ^ denexp.toInt.toNat) (poly row.toList)))

Ratpoints.Sturm.evalSign computes the sign of the value of the polynomial of the row at num / 2 ^ denexp.

theorem Ratpoints.Sturm.signCount_eq_signVariations {s : ℤ} (hs : s = -1 ∨ s = 1) {l : List ℤ} (hl : ∀ t ∈ l, t = -1 ∨ t = 0 ∨ t = 1) : signCount s l = (s :: l).signVariations

The sign changes that Ratpoints.Sturm.signsAt counts after a sign s ≠ 0 in a list of signs are the sign variations of s followed by the list.

theorem Ratpoints.Sturm.ite_add_signCount_eq_signVariations {s0 s1 : ℤ} (h0 : s0 = -1 ∨ s0 = 0 ∨ s0 = 1) (h1 : s1 = -1 ∨ s1 = 0 ∨ s1 = 1) (h01 : s0 ≠ 0 ∨ s1 ≠ 0) {l : List ℤ} (hl : ∀ t ∈ l, t = -1 ∨ t = 0 ∨ t = 1) : (if s0 * s1 = -1 then 1 else 0) + signCount (if s1 = 0 then s0 else s1) l = (s0 :: s1 :: l).signVariations

The count of Ratpoints.Sturm.signsAt from the signs s0 and s1 of f and f', not both zero, and the signs of the further rows: the sign variations of all of them.

theorem Ratpoints.Sturm.run_countsAtInfinity_eq_signVariations {rows : Array (Array ℤ)} {k : ℕ} (h : ∀ n ≤ k, rows[n]!.back! ≠ 0) : (countsAtInfinity rows k).run = ((List.map (signAtTop rows) (List.range (k + 1))).signVariations, (List.map (signAtBot rows) (List.range (k + 1))).signVariations)

The counts of Ratpoints.Sturm.countsAtInfinity for rows with nonzero leading coefficients: the sign variations of the signs of the rows 0, …, k at +∞ and at -∞.

theorem Ratpoints.Sturm.run_evalSign_eq_neg_one_or_eq_zero_or_eq_one (row : Array ℤ) (num denexp : Int64) : (evalSign row num denexp).run = -1 ∨ (evalSign row num denexp).run = 0 ∨ (evalSign row num denexp).run = 1

Ratpoints.Sturm.evalSign returns a sign.

theorem Ratpoints.Sturm.run_signsAt_eq_signVariations {rows : Array (Array ℤ)} {k : ℕ} (hk : 1 ≤ k) {nm dem : Int64} (h01 : (evalSign rows[0]! nm dem).run ≠ 0 ∨ (evalSign rows[1]! nm dem).run ≠ 0) : (signsAt rows k nm dem).run = ((evalSign rows[0]! nm dem).run, (evalSign rows[1]! nm dem).run, (List.map (fun (n : ℕ) => (evalSign rows[n]! nm dem).run) (List.range (k + 1))).signVariations)

The count of Ratpoints.Sturm.signsAt at a point where f and f' do not both vanish is the number of sign variations of the signs of the rows 0, …, k of the chain there.

The chain as a Sturm sequence

theorem Ratpoints.Sturm.IsChain.poly_toList_ne_zero {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {i : ℕ} (hi : i < ch.size) : poly ch[i]!.toList ≠ 0

theorem Ratpoints.Sturm.IsChain.posAssoc_neg_mod {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {k : ℕ} (hk : k + 2 < ch.size) : (-poly ch[k]!.toList % poly ch[k + 1]!.toList).PosAssoc (poly ch[k + 2]!.toList)

In a chain, the row k + 2 is a positive multiple of the negated remainder of the row k by the row k + 1, the entry of Polynomial.sturmSeq that follows them: by Ratpoints.Sturm.IsChain.exists_mul_eq, -s_k = (g / A) s_(k+2) - (Q / A) s_(k+1), where s_(k+2) has the smaller degree.

@[reducible, inline]

noncomputable abbrev Ratpoints.Sturm.rowPolys (ch : Array (Array ℤ)) : List (Polynomial ℚ)

The polynomials over ℚ of the rows of a chain.

Equations

• Ratpoints.Sturm.rowPolys ch = List.map (fun (r : Array ℤ) => Ratpoints.poly r.toList) ch.toList

theorem Ratpoints.Sturm.getElem_rowPolys (ch : Array (Array ℤ)) {i : ℕ} (hi : i < (rowPolys ch).length) : (rowPolys ch)[i] = poly ch[i]!.toList

theorem Ratpoints.Sturm.IsChain.forall₂_posAssoc_sturmSeq {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (h1 : ch.back!.size = 1) : List.Forall₂ Polynomial.PosAssoc (rowPolys ch) ((poly (List.take (d + 1) c)).sturmSeq (Polynomial.derivative (poly (List.take (d + 1) c))))

The rows of a chain whose last row is constant are entrywise positive multiples of the entries of the Sturm sequence of f and f', over ℚ.

@[reducible, inline]

noncomputable abbrev Ratpoints.Sturm.chainPoly (c : List ℤ) (d : ℕ) : Polynomial ℝ

The real polynomial of c that the chain of c and its degree d computes the remainder chain of, the polynomial with the coefficients c₀, …, c_d over ℝ.

Equations

• Ratpoints.Sturm.chainPoly c d = Polynomial.map (Rat.castHom ℝ) (Ratpoints.poly (List.take (d + 1) c))

theorem Ratpoints.Sturm.IsChain.forall₂_posAssoc_sturmSeq_map {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (h1 : ch.back!.size = 1) : List.Forall₂ Polynomial.PosAssoc (List.map (Polynomial.map (Rat.castHom ℝ)) (rowPolys ch)) ((chainPoly c d).sturmSeq (Polynomial.derivative (chainPoly c d)))

The real polynomials of the rows of a chain whose last row is constant are entrywise positive multiples of the entries of the Sturm sequence of f and f' over ℝ, the sequence of Ratpoints.SturmTheorem.

theorem Ratpoints.Sturm.IsChain.size_getElem!_le {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {n : ℕ} (hn : n < ch.size) : ch[n]!.size ≤ d + 1

Every row of a chain has at most d + 1 entries.

theorem Ratpoints.Sturm.IsChain.run_evalSign_eq {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (hd : d < 2 ^ 57) {n : ℕ} (hn : n < ch.size) (nm : Int64) {dem : Int64} (h0 : 0 ≤ dem.toInt) (h55 : dem.toInt ≤ 55) : (evalSign ch[n]! nm dem).run = ↑(SignType.sign (Polynomial.eval (↑(↑nm.toInt / 2 ^ dem.toInt.toNat)) (Polynomial.map (Rat.castHom ℝ) (poly ch[n]!.toList))))

Ratpoints.Sturm.evalSign computes the sign of the real polynomial of a row of a chain of a polynomial of degree d < 2 ^ 57 at nm / 2 ^ dem for 0 ≤ dem ≤ 55, the depths of the Sturm step, where the exponents stay within a long.

theorem Ratpoints.Sturm.signVariations_map_range_eq {ch : Array (Array ℤ)} {s : ℕ → ℤ} {g : Polynomial ℝ → ℝ} (hs : ∀ n < ch.size, s n = ↑(SignType.sign (g (Polynomial.map (Rat.castHom ℝ) (poly ch[n]!.toList))))) : (List.map s (List.range ch.size)).signVariations = (List.map g (List.map (Polynomial.map (Rat.castHom ℝ)) (rowPolys ch))).signVariations

Integer signs of the values of a map g at the real polynomials of the rows of a chain have the sign variations of those values.

theorem Ratpoints.Sturm.IsChain.signVariations_run_evalSign {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (h1 : ch.back!.size = 1) (hd : d < 2 ^ 57) (nm : Int64) {dem : Int64} (h0 : 0 ≤ dem.toInt) (h55 : dem.toInt ≤ 55) : (List.map (fun (n : ℕ) => (evalSign ch[n]! nm dem).run) (List.range ch.size)).signVariations = sturmV (chainPoly c d) ↑(↑nm.toInt / 2 ^ dem.toInt.toNat)

The signs that Ratpoints.Sturm.evalSign computes for the rows of a chain whose last row is constant, of a polynomial of degree d < 2 ^ 57, at nm / 2 ^ dem for 0 ≤ dem ≤ 55, have the sign variations of the Sturm sequence of the real polynomial there.

theorem Ratpoints.Sturm.IsChain.run_signsAt_eq {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (h1 : ch.back!.size = 1) (hd : d < 2 ^ 57) (hsq : Squarefree (chainPoly c d)) (nm : Int64) {dem : Int64} (h0 : 0 ≤ dem.toInt) (h55 : dem.toInt ≤ 55) : (signsAt ch (ch.size - 1) nm dem).run = (↑(SignType.sign (Polynomial.eval (↑(↑nm.toInt / 2 ^ dem.toInt.toNat)) (chainPoly c d))), ↑(SignType.sign (Polynomial.eval (↑(↑nm.toInt / 2 ^ dem.toInt.toNat)) (Polynomial.derivative (chainPoly c d)))), sturmV (chainPoly c d) ↑(↑nm.toInt / 2 ^ dem.toInt.toNat))

At m = nm / 2 ^ dem, 0 ≤ dem ≤ 55, Ratpoints.Sturm.signsAt on a chain whose last row is constant, of a polynomial of degree d < 2 ^ 57 that is squarefree over ℝ, computes the signs of f(m) and f'(m) and the count V(m) of the Sturm sequence over ℝ.

theorem Ratpoints.Sturm.IsChain.sign_leadingCoeff_map {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {n : ℕ} (hn : n < ch.size) : ↑(SignType.sign (Polynomial.map (Rat.castHom ℝ) (poly ch[n]!.toList)).leadingCoeff) = signAtTop ch n

The sign of the leading coefficient of the real polynomial of a row of a chain is the sign of the row at +∞ of Ratpoints.Sturm.countsAtInfinity.

theorem Ratpoints.Sturm.IsChain.sign_neg_one_pow_mul_leadingCoeff_map {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) {n : ℕ} (hn : n < ch.size) : ↑(SignType.sign ((-1) ^ (Polynomial.map (Rat.castHom ℝ) (poly ch[n]!.toList)).natDegree * (Polynomial.map (Rat.castHom ℝ) (poly ch[n]!.toList)).leadingCoeff)) = signAtBot ch n

The sign at -∞ of the real polynomial of a row of a chain, (-1) ^ deg times the sign of its leading coefficient, is the sign of the row at -∞ of Ratpoints.Sturm.countsAtInfinity.

theorem Ratpoints.Sturm.IsChain.run_countsAtInfinity_eq {c : List ℤ} {d : ℕ} {ch : Array (Array ℤ)} (h : IsChain c d ch) (h1 : ch.back!.size = 1) : (countsAtInfinity ch (ch.size - 1)).run = (vTop (chainPoly c d), vBot (chainPoly c d))

For a chain whose last row is constant, the counts of Ratpoints.Sturm.countsAtInfinity are the counts V(+∞) and V(-∞) of the Sturm sequence of the real polynomial.