Virtual roots of a real polynomial

The virtual roots of González-Vega, Lombardi and Mahé are, for a real polynomial P of degree d, d real numbers ρ_{d,1}(P) ≤ … ≤ ρ_{d,d}(P) that coincide with the real roots when P has d of them. They are built recursively from the virtual roots of P': between two consecutive breakpoints a ≤ b, the operator ℛ_d(a, b, P) returns a point of [a, b] where |P| is minimal, which is a root of P whenever P has one in [a, b].

The construction here works on a fixed interval [lo, hi] that serves as the outer breakpoints.

Main definitions

• VirtualRoots.R p a b: a minimizer of |p| on [a, b] (the operator ℛ_d).
• VirtualRoots.vroots lo hi p: the list of virtual roots of p.

Main results

• VirtualRoots.R_mem, VirtualRoots.R_isMinOn, VirtualRoots.R_eval_eq_zero_of_exists: ℛ_d lies in [a, b], minimizes |p|, and is a root when p has one in [a, b].
• VirtualRoots.vroots_length: a polynomial of degree d has exactly d virtual roots.
• VirtualRoots.vroots_isChain, VirtualRoots.vroots_subset_Icc: they are sorted and lie in [lo, hi].
• VirtualRoots.vroots_interlacing: the interlacing ρ_{d,r}(P) ≤ ρ_{d-1,r}(P') ≤ ρ_{d,r+1}(P) (Coste, Prop. 2.3).

References

• L. González-Vega, H. Lombardi, L. Mahé, Virtual roots of real polynomials, J. Pure Appl. Algebra 124 (1998) 147–166.
• M. Coste, T. Lajous-Loaeza, H. Lombardi, M.-F. Roy, Generalized Budan–Fourier theorem and virtual roots, J. Complexity 21 (2005) 479–486.

The monotonicity bedrock of ℛ_d

On an interval where P' keeps a constant nonzero sign, P is strictly monotone. This is exactly the hypothesis under which ℛ_d(a,b,P) is defined, and it is what makes the minimiser of |P| on [a,b] unique: either the single root (if P changes sign across the interval) or the endpoint nearer to zero. The two lemmas below are the analytic foundation; they reuse the mean-value engine already used in BudanFourier for the sign analysis.

theorem VirtualRoots.eval_strictMonoOn_of_derivative_pos {p : Polynomial ℝ} {a b : ℝ} (h : ∀ x ∈ Set.Icc a b, 0 < Polynomial.eval x (Polynomial.derivative p)) : StrictMonoOn (fun (x : ℝ) => Polynomial.eval x p) (Set.Icc a b)

Where the derivative is positive on [a,b], P is strictly increasing there.

theorem VirtualRoots.eval_strictAntiOn_of_derivative_neg {p : Polynomial ℝ} {a b : ℝ} (h : ∀ x ∈ Set.Icc a b, Polynomial.eval x (Polynomial.derivative p) < 0) : StrictAntiOn (fun (x : ℝ) => Polynomial.eval x p) (Set.Icc a b)

Where the derivative is negative on [a,b], P is strictly decreasing there.

theorem VirtualRoots.exists_isMinOn_abs_eval {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) : ∃ z ∈ Set.Icc a b, IsMinOn (fun (x : ℝ) => |Polynomial.eval x p|) (Set.Icc a b) z

|P| attains a minimum on a nonempty closed interval. The existence half of ℛ_d: a continuous function on the compact [a,b] reaches its infimum. (Uniqueness of the minimiser comes from strict monotonicity above, when P' keeps a constant sign.)

The choice operator ℛ_d

R p a b is Coste's ℛ_d(a,b,P): a point of [a,b] minimising |P|. On an interval where P' keeps a constant sign (so P is strictly monotone, by the bedrock above) this minimiser is unique, and equals the unique root of P there when one exists, otherwise the nearer endpoint. We define it by choosing a minimiser (which exists by exists_isMinOn_abs_eval) and prove the two properties that matter downstream: it lands in [a,b] (the engine of the Rolle interlacing) and it is a root of P whenever P has one in [a,b] (so virtual roots extend actual roots, Coste's Prop. 2.2).

noncomputable def VirtualRoots.R (p : Polynomial ℝ) (a b : ℝ) : ℝ

The choice operator ℛ_d(a,b,P): a minimiser of |P| on [a,b] (junk value a if b<a).

Equations

• VirtualRoots.R p a b = if hab : a ≤ b then ⋯.choose else a

theorem VirtualRoots.R_mem {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) : R p a b ∈ Set.Icc a b

ℛ_d(a,b,P) lands in [a,b]. This single fact yields the Rolle interlacing of virtual roots, since ρ_{d,j}(P) = ℛ_d(ρ_{d-1,j-1}(P'),ρ_{d-1,j}(P'),P) then lies between consecutive virtual roots of P'.

theorem VirtualRoots.R_isMinOn {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) : IsMinOn (fun (x : ℝ) => |Polynomial.eval x p|) (Set.Icc a b) (R p a b)

ℛ_d(a,b,P) minimises |P| on [a,b].

theorem VirtualRoots.R_eval_eq_zero_of_exists {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (h : ∃ z ∈ Set.Icc a b, Polynomial.eval z p = 0) : Polynomial.eval (R p a b) p = 0

ℛ_d captures actual roots. If P vanishes somewhere in [a,b], then ℛ_d(a,b,P) is a root of P: the minimum of |P| is then 0, so the minimiser is a zero. (No monotonicity needed; this is the half of Coste's Prop. 2.2 saying virtual roots extend the actual ones.)

The root case of ℛ_d

When P changes sign across the interval, ℛ_d(a,b,P) is an actual root of P. This is the case that makes a virtual root coincide with a real root, and it is what the recursive ρ produces on each P'-monotone interval on which P crosses zero. It follows from the intermediate value theorem (existence of a root) and R_eval_eq_zero_of_exists.

theorem VirtualRoots.R_eval_eq_zero_of_le_zero_le {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (ha : Polynomial.eval a p ≤ 0) (hb : 0 ≤ Polynomial.eval b p) : Polynomial.eval (R p a b) p = 0

If P(a) ≤ 0 ≤ P(b) on [a,b], then ℛ_d(a,b,P) is a root of P.

theorem VirtualRoots.R_eval_eq_zero_of_ge_zero_ge {p : Polynomial ℝ} {a b : ℝ} (hab : a ≤ b) (ha : 0 ≤ Polynomial.eval a p) (hb : Polynomial.eval b p ≤ 0) : Polynomial.eval (R p a b) p = 0

If P(b) ≤ 0 ≤ P(a) on [a,b], then ℛ_d(a,b,P) is a root of P.

The recursive virtual roots

On a bracketing interval [lo,hi] that contains all roots of the whole derivative tower (take lo = -M, hi = M with M a Cauchy bound Polynomial.cauchyBound, design (B)), the d virtual roots of P are built from the d-1 virtual roots of P': the breakpoints lo, ρ_{d-1,1}(P'), …, ρ_{d-1,d-1}(P'), hi cut [lo,hi] into d intervals, on each of which P' keeps a constant sign, and ρ_{d,j}(P) is ℛ_d applied to the j-th. Working on the finite [lo,hi] keeps everything over ℝ and reuses R/R_mem/R_eval_* verbatim.

@[irreducible]

noncomputable def VirtualRoots.vroots (lo hi : ℝ) (p : Polynomial ℝ) : List ℝ

The recursive virtual roots of p on the bracketing interval [lo,hi], built from the virtual roots of derivative p by ℛ_d on each P'-monotone subinterval. A degree-0 polynomial has none; well-founded on natDegree (natDegree_derivative_lt).

Equations

• One or more equations did not get rendered due to their size.

theorem VirtualRoots.vroots_eq_zipWith {lo hi : ℝ} {p : Polynomial ℝ} (hd : p.natDegree ≠ 0) : vroots lo hi p = List.zipWith (R p) (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])) (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])).tail

The vroots recursion, exposed. For deg p ≥ 1, the virtual roots are ℛ_d applied to consecutive breakpoints lo :: (vroots p' ++ [hi]). Stated so other modules can unfold the (non- @[expose]) vroots definition through a lemma.

theorem VirtualRoots.natDegree_derivative_eq {p : Polynomial ℝ} (hp : 0 < p.natDegree) : (Polynomial.derivative p).natDegree = p.natDegree - 1

Exact derivative degree in characteristic zero: deg(P') = deg P − 1 for deg P ≥ 1.

theorem VirtualRoots.vroots_length (lo hi : ℝ) (p : Polynomial ℝ) : (vroots lo hi p).length = p.natDegree

vroots has the right length: a degree-d polynomial has exactly d virtual roots.

theorem VirtualRoots.isChain_zipWith_R (p : Polynomial ℝ) (bps : List ℝ) : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) bps → List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (List.zipWith (R p) bps bps.tail)

Virtual roots come out sorted (combinatorial core of the interlacing). If the breakpoints are sorted, the ℛ_d-values between consecutive ones are sorted too: each R p bps[j] bps[j+1] lies in [bps[j], bps[j+1]] (by R_mem), and consecutive values are separated by the shared breakpoint bps[j+1] — exactly the Rolle interlacing ρ_{d,j} ≤ bps[j+1] ≤ ρ_{d,j+1}.

The breakpoints invariant

The recursion that builds vroots is driven by one invariant: the augmented list lo :: (vroots lo hi p ++ [hi]) — the breakpoints that cut [lo,hi] for the polynomial one degree up — is sorted, and every virtual root lands in [lo,hi]. The two facts are mutually dependent (a breakpoint list is sorted only if its members lie in range, and an ℛ_d-value lies in range only between sorted breakpoints), so they are proved together by one induction down the derivative tower. The chain half is the Rolle interlacing ρ_{d,r}(P) ≤ ρ_{d-1,r}(P') ≤ ρ_{d,r+1}(P) in list form.

theorem VirtualRoots.vroots_chain_mem (lo hi : ℝ) (hab : lo ≤ hi) (p : Polynomial ℝ) : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (lo :: (vroots lo hi p ++ [hi])) ∧ ∀ x ∈ vroots lo hi p, x ∈ Set.Icc lo hi

The breakpoints invariant. For lo ≤ hi, the augmented breakpoint list lo :: (vroots lo hi p ++ [hi]) is sorted, and every virtual root of p lies in [lo,hi]. Proved by one induction down the tower: the breakpoints for p are exactly this list for derivative p.

theorem VirtualRoots.vroots_isChain (lo hi : ℝ) (hab : lo ≤ hi) (p : Polynomial ℝ) : List.IsChain (fun (x1 x2 : ℝ) => x1 ≤ x2) (lo :: (vroots lo hi p ++ [hi]))

The virtual roots come out sorted on [lo,hi] (Rolle interlacing, list form): the breakpoint list lo :: (vroots lo hi p ++ [hi]) for the next degree up is a chain.

theorem VirtualRoots.vroots_subset_Icc (lo hi : ℝ) (hab : lo ≤ hi) (p : Polynomial ℝ) (x : ℝ) : x ∈ vroots lo hi p → x ∈ Set.Icc lo hi

Every virtual root lies in the bracketing interval [lo,hi].

The index-form interlacing

The sorted invariant says the virtual roots are ordered; the sharper statement is where each one sits. With bps = lo :: (vroots lo hi P' ++ [hi]) the breakpoints cutting [lo,hi] for P, the r-th virtual root of P lands in [bps[r], bps[r+1]] — that is ℛ_d landing in its own interval, read index by index. Since the interior breakpoints bps[r+1] are exactly the virtual roots of P', this is the Rolle interlacing ρ_{d,r}(P) ≤ ρ_{d-1,r}(P') ≤ ρ_{d,r+1}(P).

theorem VirtualRoots.vroots_getElem_mem (lo hi : ℝ) (hab : lo ≤ hi) (p : Polynomial ℝ) (r : ℕ) (hr : r < (vroots lo hi p).length) (hb : r + 1 < (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi])).length) : (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[r] ≤ (vroots lo hi p)[r] ∧ (vroots lo hi p)[r] ≤ (lo :: (vroots lo hi (Polynomial.derivative p) ++ [hi]))[r + 1]

Each virtual root lies between its two breakpoints (Coste's localization of ρ_{d,r}): for bps = lo :: (vroots lo hi P' ++ [hi]), one has bps[r] ≤ (vroots lo hi P)[r] ≤ bps[r+1].

theorem VirtualRoots.vroots_interlacing (lo hi : ℝ) (hab : lo ≤ hi) (p : Polynomial ℝ) (r : ℕ) (hr' : r < (vroots lo hi (Polynomial.derivative p)).length) (hrp : r + 1 < (vroots lo hi p).length) : (vroots lo hi p)[r] ≤ (vroots lo hi (Polynomial.derivative p))[r] ∧ (vroots lo hi (Polynomial.derivative p))[r] ≤ (vroots lo hi p)[r + 1]

The Rolle interlacing of virtual roots (Coste, Prop. 2.3), in list/index form: ρ_{d,r}(P) ≤ ρ_{d-1,r}(P') ≤ ρ_{d,r+1}(P). Each virtual root of P' is wedged between two consecutive virtual roots of P, because the P'-roots are exactly the interior breakpoints that ℛ_d interpolates.