The exact Budan–Fourier count for virtual roots

The number of virtual roots of a nonzero real polynomial p in (a, b] equals the Budan–Fourier drop V(a) - V(b) of the derivative tower. This turns the inequality of BudanFourier.budan_fourier into an equality.

The proof shows V(x) = #{virtual roots of p greater than x} by induction down the derivative tower; the step VirtualRoots.count_step compares the leading sign variation of the tower of p with the virtual root that the interlacing places above x.

Main definitions

• VirtualRoots.Brackets lo hi p: every root of every member of the derivative tower of p lies in (lo, hi).

Main results

• VirtualRoots.fourierVar_eq_card_vroots_gt: fourierVar p x is the number of virtual roots of p greater than x, for x ∈ [lo, hi).
• VirtualRoots.card_vroots_Ioc_eq_fourierVar: the number of virtual roots in (a, b] is fourierVar p a - fourierVar p b.

References

• M. Coste, T. Lajous-Loaeza, H. Lombardi, M.-F. Roy, Generalized Budan–Fourier theorem and virtual roots, J. Complexity 21 (2005) 479–486.

def VirtualRoots.Brackets (lo hi : ℝ) (p : Polynomial ℝ) : Prop

Bracketing hypothesis. [lo,hi] strictly contains every root of every member of the derivative tower of p. Then (as the count needs) all virtual roots lie in (lo,hi), V(lo) is the degree, and V(hi) = 0.

Equations

• VirtualRoots.Brackets lo hi p = ∀ q ∈ BudanFourier.fourierSeq p, ∀ (z : ℝ), Polynomial.eval z q = 0 → z ∈ Set.Ioo lo hi

theorem VirtualRoots.fourierSeq_cons {p : Polynomial ℝ} (hp : 0 < p.natDegree) : BudanFourier.fourierSeq p = p :: BudanFourier.fourierSeq (Polynomial.derivative p)

The derivative tower of p is p followed by the tower of p' (for deg p ≥ 1). The structural recursion that lets fourierVar and vroots be compared one degree at a time.

theorem VirtualRoots.fourierVar_succ_root {p : Polynomial ℝ} (hp : 0 < p.natDegree) {x : ℝ} (hx : Polynomial.eval x p = 0) : BudanFourier.fourierVar p x = BudanFourier.fourierVar (Polynomial.derivative p) x

fourierVar recursion, root case. Where p vanishes, its sign-variation count equals that of p': the leading zero is invisible.

theorem VirtualRoots.fourierVar_succ_ne {p : Polynomial ℝ} (hp : 0 < p.natDegree) {x : ℝ} (hx : Polynomial.eval x p ≠ 0) {d : SignType} (hd : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval x q)) (BudanFourier.fourierSeq (Polynomial.derivative p)))).head? = some d) : BudanFourier.fourierVar p x = BudanFourier.fourierVar (Polynomial.derivative p) x + if SignType.sign (Polynomial.eval x p) = d then 0 else 1

fourierVar recursion, non-root case. Where p(x) ≠ 0, prepending its sign to the p'-tower adds one variation iff that sign disagrees with the first surviving sign d of the p'-tower.

theorem VirtualRoots.countP_gt_le_of_forall₂ (x : ℝ) {L M : List ℝ} (h : List.Forall₂ (fun (x1 x2 : ℝ) => x1 ≤ x2) L M) : List.countP (fun (r : ℝ) => decide (x < r)) L ≤ List.countP (fun (r : ℝ) => decide (x < r)) M

Count-above is monotone under a pointwise ≤. If L[i] ≤ M[i] entrywise, then at most as many of L exceed x as of M. The signless engine of the vroots-side recursion.

theorem VirtualRoots.card_filter_gt_eq_countP (x : ℝ) (L : List ℝ) : (Multiset.filter (fun (r : ℝ) => x < r) ↑L).card = List.countP (fun (r : ℝ) => decide (x < r)) L

Bridge: the Multiset-card form of N(x) equals the List.countP form the engine uses.

theorem VirtualRoots.natDegree_derivative_eq' (p : Polynomial ℝ) : (Polynomial.derivative p).natDegree = p.natDegree - 1

The derivative drops the degree by exactly one (characteristic zero), even at degree 0.

theorem VirtualRoots.N_deriv_le_N {lo hi : ℝ} (hab : lo ≤ hi) (p : Polynomial ℝ) (x : ℝ) : (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi (Polynomial.derivative p))).card ≤ (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi p)).card

Lower bound of the vroots-side recursion. N_{p'}(x) ≤ N_p(x): each virtual root of p' above x is matched by one of p above x (the right half of the interlacing).

theorem VirtualRoots.N_le_N_deriv_succ {lo hi : ℝ} (hab : lo ≤ hi) (p : Polynomial ℝ) (x : ℝ) : (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi p)).card ≤ (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi (Polynomial.derivative p))).card + 1

Upper bound of the vroots-side recursion. N_p(x) ≤ N_{p'}(x) + 1: dropping the top virtual root of p, the rest are dominated by those of p' (the left half of the interlacing).

theorem VirtualRoots.signChanges_le_cons (c : SignType) (s : List SignType) : Sturm.signChanges s ≤ Sturm.signChanges (c :: s)

Prepending a sign can only add variations: signChanges is monotone under cons (a leading nonzero sign adds 0 or 1; a leading zero adds nothing).

theorem VirtualRoots.fourierVar_deriv_le {p : Polynomial ℝ} (hp : 0 < p.natDegree) (x : ℝ) : BudanFourier.fourierVar (Polynomial.derivative p) x ≤ BudanFourier.fourierVar p x

The derivative's Fourier count never exceeds p's: the extra leading derivative p contributes at most one new sign variation. The monotonicity that makes the count recursion telescope.

Toward count_step: foundational lemmas

The key step needs that p is strictly monotone on each p'-cell, which needs p' to be sign-constant there, which needs Coste's Prop. 2.2: every actual root of a polynomial is one of its virtual roots. These lemmas build toward it: brackets_ne_zero, brackets_derivative (the bracket hypothesis descends the tower), and exists_deriv_root_between (Rolle: a root of q' between any two roots of q).

theorem VirtualRoots.brackets_ne_zero {lo hi : ℝ} {q : Polynomial ℝ} (hbr : Brackets lo hi q) : q ≠ 0

A bracketed polynomial is nonzero (0 would force the right endpoint hi into the open interval (lo,hi)).

theorem VirtualRoots.brackets_derivative {lo hi : ℝ} {q : Polynomial ℝ} (hq : 0 < q.natDegree) (hbr : Brackets lo hi q) : Brackets lo hi (Polynomial.derivative q)

The bracket hypothesis descends to the derivative (its Fourier sequence is a tail of q's, for deg q ≥ 1).

theorem VirtualRoots.exists_deriv_root_between {q : Polynomial ℝ} {z z' : ℝ} (hlt : z < z') (hz : Polynomial.eval z q = 0) (hz' : Polynomial.eval z' q = 0) : ∃ y ∈ Set.Ioo z z', Polynomial.eval y (Polynomial.derivative q) = 0

Rolle for the derivative tower. Between any two roots of q there is a root of q'.

theorem VirtualRoots.not_mem_between {L : List ℝ} (hL : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) L) {i : ℕ} (hi : i + 1 < L.length) {y : ℝ} (hy : y ∈ L) (h1 : L[i] < y) (h2 : y < L[i + 1]) : False

A sorted list has no member strictly between two consecutive entries. The combinatorial fact that pins each q'-root (which Coste 2.2 places among the breakpoints) to a breakpoint, never strictly inside a cell.

theorem VirtualRoots.exists_bracket {z : ℝ} (L : List ℝ) (hchain : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) L) (hne : L ≠ []) (hlo : L.head hne ≤ z) (hhi : z ≤ L.getLast hne) (hlen : 2 ≤ L.length) : ∃ (i : ℕ) (h : i + 1 < L.length), L[i] ≤ z ∧ z ≤ L[i + 1]

Cell location. In a sorted list of length ≥ 2 spanning z (head ≤ z ≤ last), some consecutive pair brackets z. Locates the cell of the breakpoint partition that contains a root.

theorem VirtualRoots.root_mem_vroots {lo hi : ℝ} (hab : lo ≤ hi) {q : Polynomial ℝ} (hbr : Brackets lo hi q) {z : ℝ} (hz : Polynomial.eval z q = 0) : z ∈ vroots lo hi q

Coste's Proposition 2.2. Every actual root of q (under the bracket hypothesis) is one of its virtual roots. The keystone: it makes the breakpoints capture all of q''s roots, so q' is sign-constant on each cell and q is monotone there. Proved by strong induction down the tower: locate the root's cell (exists_bracket), capture it with ℛ_d (R_eval_eq_zero_of_exists), and rule out a second root by Rolle (exists_deriv_root_between gives a q'-root in the open cell, which the inductive hypothesis places among the breakpoints — impossible by not_mem_between).

(a)+(b): p is strictly monotone on each p'-cell

Coste 2.2 makes p' root-free on each open cell; with the IVT that forces p' to keep a constant sign there, hence (by the mean-value bedrock) p is strictly monotone across the closed cell — even though p' may vanish at the breakpoint endpoints.

theorem VirtualRoots.exists_root_of_sign_change {q : Polynomial ℝ} {c d : ℝ} (hcd : c < d) (hsign : Polynomial.eval c q * Polynomial.eval d q < 0) : ∃ e ∈ Set.Ioo c d, Polynomial.eval e q = 0

IVT sign-change. A continuous polynomial with opposite signs at the ends of an interval has a root strictly inside.

theorem VirtualRoots.strictMonoOn_or_antiOn_of_no_deriv_root {p : Polynomial ℝ} {a b : ℝ} (hab : a < b) (hno : ∀ y ∈ Set.Ioo a b, Polynomial.eval y (Polynomial.derivative p) ≠ 0) : StrictMonoOn (fun (x : ℝ) => Polynomial.eval x p) (Set.Icc a b) ∨ StrictAntiOn (fun (x : ℝ) => Polynomial.eval x p) (Set.Icc a b)

(a)+(b): monotone on a root-free cell. If p' has no root on the open interval (a,b), then p is strictly monotone (one way or the other) on the closed [a,b].

(c): the count increment is the cell indicator

With the breakpoints sorted, the virtual roots above x are a tail: every cell strictly above x contributes its root, every cell strictly below contributes nothing, and only the cell containing x is in question. So N_p(x) − N_{p'}(x) is exactly whether the virtual root of p in x's cell lies above x.

theorem VirtualRoots.exists_bracket_lt {z : ℝ} (L : List ℝ) (hchain : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) L) (hne : L ≠ []) (hlo : L.head hne ≤ z) (hhi : z < L.getLast hne) (hlen : 2 ≤ L.length) : ∃ (i : ℕ) (h : i + 1 < L.length), L[i] ≤ z ∧ z < L[i + 1]

Half-open cell location. In a sorted list of length ≥ 2 with head ≤ z < last, some consecutive pair half-open-brackets z (L[i] ≤ z < L[i+1]).

theorem VirtualRoots.countP_gt_of_split (x : ℝ) (L : List ℝ) (k : ℕ) : k ≤ L.length → (∀ (j : ℕ) (h : j < L.length), j < k → L[j] ≤ x) → (∀ (j : ℕ) (h : j < L.length), k ≤ j → x < L[j]) → List.countP (fun (r : ℝ) => decide (x < r)) L = L.length - k

Threshold count. If a list splits at index k into a ≤ x prefix and a > x suffix, then the number of entries exceeding x is length − k.

theorem VirtualRoots.chain_getElem_mono {L : List ℝ} (hL : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) L) {s t : ℕ} (hst : s ≤ t) (ht : t < L.length) : L[s] ≤ L[t]

A chain (≤-sorted list) is monotone in its index.

theorem VirtualRoots.deriv_vroot_eq_bps {lo hi : ℝ} {p : Polynomial ℝ} {j : ℕ} (hj : j < (vroots lo hi (Polynomial.derivative p)).length) (hb : j + 1 < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])).length) : (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[j + 1] = (vroots lo hi (Polynomial.derivative p))[j]

The j-th virtual root of p' is the (j+1)-th breakpoint of the partition bps = lo :: vroots(p') ++ [hi].

theorem VirtualRoots.count_diff_eq_cell {lo hi : ℝ} (hab : lo ≤ hi) {p : Polynomial ℝ} (hp : 0 < p.natDegree) {x : ℝ} {i : ℕ} (hiv : i < (vroots lo hi p).length) (hi1 : i + 1 < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])).length) (hbiz : (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[i] ≤ x) (hzbi : x < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[i + 1]) : List.countP (fun (r : ℝ) => decide (x < r)) (vroots lo hi p) = List.countP (fun (r : ℝ) => decide (x < r)) (vroots lo hi (Polynomial.derivative p)) + if x < (vroots lo hi p)[i] then 1 else 0

(c) The count increment is the cell indicator. With x located in the cell [bps[i], bps[i+1]] of the p'-breakpoint partition (bps = lo :: vroots(p') ++ [hi]), the number of virtual roots of p strictly above x exceeds that of p' by exactly whether the virtual root of p sitting in that cell lies above x. Purely combinatorial: the interlacing forces every cell above x to contribute a root, every cell below to contribute none, and only x's own cell to be in question.

(d) lemmas: the cell is p'-root-free and pins v_i to the sign of p(x)

theorem VirtualRoots.deriv_root_free_on_cell {lo hi : ℝ} (hab : lo ≤ hi) {p : Polynomial ℝ} (hp : 0 < p.natDegree) (hbr : Brackets lo hi p) {i : ℕ} (hi1 : i + 1 < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])).length) {y : ℝ} (hy1 : (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[i] < y) (hy2 : y < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[i + 1]) : Polynomial.eval y (Polynomial.derivative p) ≠ 0

(d) p' is root-free on the open cell. Any root of p' strictly inside a cell would (Coste 2.2) be a virtual root of p', i.e. a breakpoint — impossible strictly between two consecutive breakpoints.

theorem VirtualRoots.lt_R_iff_eval_neg {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (hmono : StrictMonoOn (fun (t : ℝ) => Polynomial.eval t p) (Set.Icc a b)) {x : ℝ} (hx : x ∈ Set.Ico a b) : x < R p a b ↔ Polynomial.eval x p < 0

(d) On an increasing cell, v_i sits above x iff p(x) < 0. The |p|-minimiser ℛ_d of a strictly increasing p lies right of x exactly when p is still negative at x.

theorem VirtualRoots.lt_R_iff_eval_pos {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (hanti : StrictAntiOn (fun (t : ℝ) => Polynomial.eval t p) (Set.Icc a b)) {x : ℝ} (hx : x ∈ Set.Ico a b) : x < R p a b ↔ 0 < Polynomial.eval x p

(d) On a decreasing cell, v_i sits above x iff p(x) > 0. The mirror of lt_R_iff_eval_neg for a strictly decreasing p.

(d) The right-gap: a point z just above x avoiding all tower roots

signs_right_eq_Rseq needs a point z > x at which no member of the derivative tower vanishes on (x, z]. Such a z exists because each (nonzero) tower member has finitely many roots.

theorem VirtualRoots.exists_gap_right_single {q : Polynomial ℝ} (hq : q ≠ 0) {x B : ℝ} (hxB : x < B) : ∃ (z : ℝ), x < z ∧ z ≤ B ∧ ∀ w ∈ Set.Ioc x z, Polynomial.eval w q ≠ 0

A single nonzero polynomial has a root-free half-open interval (x, z] for some z ≤ B.

theorem VirtualRoots.exists_tower_gap_right (L : List (Polynomial ℝ)) : (∀ q ∈ L, q ≠ 0) → ∀ {x B : ℝ}, x < B → ∃ (z : ℝ), x < z ∧ z ≤ B ∧ ∀ q ∈ L, ∀ w ∈ Set.Ioc x z, Polynomial.eval w q ≠ 0

The right-gap for a tower. For a finite list of nonzero polynomials and x < B, some z ∈ (x, B] has every member root-free on (x, z].

theorem VirtualRoots.deriv_sign_const_on_cell {p : Polynomial ℝ} {a b : ℝ} (hno : ∀ w ∈ Set.Ioo a b, Polynomial.eval w (Polynomial.derivative p) ≠ 0) {w₁ w₂ : ℝ} (h1 : w₁ ∈ Set.Ioo a b) (h2 : w₂ ∈ Set.Ioo a b) : SignType.sign (Polynomial.eval w₁ (Polynomial.derivative p)) = SignType.sign (Polynomial.eval w₂ (Polynomial.derivative p))

p' keeps a constant sign across a root-free cell. Two interior points of a p'-root-free cell give p' the same sign (IVT).

theorem VirtualRoots.fourier_head_right {p : Polynomial ℝ} (hp' : Polynomial.derivative p ≠ 0) {x z : ℝ} (hxz : x < z) (hno : ∀ q ∈ BudanFourier.fourierSeq (Polynomial.derivative p), ∀ w ∈ Set.Ioc x z, Polynomial.eval w q ≠ 0) : (List.filter (fun (x : SignType) => decide (x ≠ 0)) (List.map (fun (q : Polynomial ℝ) => SignType.sign (Polynomial.eval x q)) (BudanFourier.fourierSeq (Polynomial.derivative p)))).head? = some (SignType.sign (Polynomial.eval z (Polynomial.derivative p)))

(d) The Fourier head d is the sign of p' just right of x. The first surviving sign of the p'-tower at x equals sign (p'(z)) for any z just above x at which no tower member vanishes on (x,z] — by signs_right_eq_Rseq (the pattern at z is Rseq of the pattern at x, whose head is the first surviving sign).

theorem VirtualRoots.count_step {lo hi : ℝ} {p : Polynomial ℝ} (hp : 0 < p.natDegree) (hbr : Brackets lo hi p) {x : ℝ} (hx : x ∈ Set.Ico lo hi) : (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi p)).card = (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi (Polynomial.derivative p))).card + (BudanFourier.fourierVar p x - BudanFourier.fourierVar (Polynomial.derivative p) x)

THE key step (the one remaining analytic fact). The increment in the count of virtual roots above x going from p' to p equals the Fourier increment V_p − V_{p'}. Geometrically: the interlacing inserts a virtual root of p above x iff the virtual root of p in x's own p'-cell lies above x, and that happens exactly when the leading sign of p at x produces a new Fourier variation. Both recursions are pinned to {0,1} (the Fourier side by fourierVar_deriv_le, the count side by N_deriv_le_N/N_le_N_deriv_succ); this lemma says the two bits agree.

theorem VirtualRoots.fourierVar_eq_card_vroots_gt {lo hi : ℝ} {p : Polynomial ℝ} (hp : p ≠ 0) (hbr : Brackets lo hi p) {x : ℝ} (hx : x ∈ Set.Ico lo hi) : BudanFourier.fourierVar p x = (Multiset.filter (fun (r : ℝ) => x < r) ↑(vroots lo hi p)).card

Core reformulation. The Budan–Fourier count at x equals the number of virtual roots of p strictly above x, by induction down the derivative tower with step count_step.

theorem VirtualRoots.card_vroots_Ioc_eq_fourierVar {lo hi : ℝ} {p : Polynomial ℝ} (hp : p ≠ 0) (hbr : Brackets lo hi p) {a b : ℝ} (ha : a ∈ Set.Ico lo hi) (hb : b ∈ Set.Ico lo hi) (hab : a ≤ b) : (Multiset.filter (fun (r : ℝ) => a < r ∧ r ≤ b) ↑(vroots lo hi p)).card = BudanFourier.fourierVar p a - BudanFourier.fourierVar p b

The exact virtual-root count. The number of virtual roots in (a,b] equals the Budan–Fourier drop V(a) − V(b), turning the inequality of BudanFourier.budan_fourier into an equality.