Descartes' sign variations as the Budan–Fourier count at zero

The number of sign variations of the derivative tower of p at 0 equals the number of sign variations of the coefficients of p, the quantity Polynomial.signVariations p of Mathlib's Descartes rule of signs. The tower evaluated at 0 has the signs of the coefficients (p^(k)(0) = k! a_k) listed from low to high degree, and the number of sign variations is invariant under reversal.

Main results

• BudanFourier.signChanges_reverse: the number of sign variations of a list of signs is invariant under reversal.
• BudanFourier.fourierVar_zero_eq_signVariations: fourierVar p 0 = Polynomial.signVariations p.

signChanges is reversal-invariant

theorem BudanFourier.filter_ne_zero_reverse (s : List SignType) : List.filter (fun (x : SignType) => decide (x ≠ 0)) s.reverse = (List.filter (fun (x : SignType) => decide (x ≠ 0)) s).reverse

filter (· ≠ 0) commutes with reverse.

theorem BudanFourier.destutter_ne_length_reverse (L : List SignType) : (List.destutter (fun (x1 x2 : SignType) => x1 ≠ x2) L.reverse).length = (List.destutter (fun (x1 x2 : SignType) => x1 ≠ x2) L).length

The number of maximal ≠-runs is the same forwards and backwards: destutter (· ≠ ·) returns a maximal ≠-chain sublist, and reversal bijects chain sublists.

theorem BudanFourier.signChanges_reverse (s : List SignType) : Sturm.signChanges s.reverse = Sturm.signChanges s

signChanges does not depend on the orientation of the list.

The tower at 0 reads the coefficient signs

theorem BudanFourier.sign_iterate_derivative_eval_zero (p : Polynomial ℝ) (k : ℕ) : SignType.sign (Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] p)) = SignType.sign (p.coeff k)

sign (p^{(k)}(0)) = sign (a_k), since p^{(k)}(0) = k!\,a_k and k! > 0.

theorem BudanFourier.fourierSeq_eval_zero_signs (p : Polynomial ℝ) : List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval 0 q)) (fourierSeq p) = List.map (fun (k : ℕ) => SignType.sign (p.coeff k)) (List.range (p.natDegree + 1))

The tower's signs at 0, as a list, are the coefficient signs [sign a_0, …, sign a_n].

theorem BudanFourier.coeffList_signs_eq_reverse (p : Polynomial ℝ) (hp : p ≠ 0) : List.map (⇑SignType.sign) p.coeffList = (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval 0 q)) (fourierSeq p)).reverse

Mathlib's coefficient sign list is the reverse of the tower's sign list (high-to-low vs low-to-high).

Descartes' count is the engine's V(0)

theorem BudanFourier.fourierVar_zero_eq_signVariations (p : Polynomial ℝ) (hp : p ≠ 0) : fourierVar p 0 = p.signVariations

Descartes through the engine. The Budan–Fourier sign-variation count of p at 0 equals the coefficient sign-variation count Polynomial.signVariations p of Descartes' rule of signs.