Polynomial interlacing

Let $f$ and $g$ be nonzero real-rooted polynomials with roots $s_1 \leq \dotsb \leq s_k$ and $r_1 \leq \dotsb \leq r_m$, listed with multiplicity. We write $f \ll g$ (StrictInterl f g) if either

$m = k + 1$ and $r_1 \leq s_1 \leq r_2 \leq s_2 \leq \dotsb \leq s_k \leq r_{k+1}$, or
$m = k$ and $s_1 \leq r_1 \leq s_2 \leq r_2 \leq \dotsb \leq s_k \leq r_k$.

In both cases $g$ has the largest root. Shared and repeated roots are allowed. The relation Interl f g also holds when $f$ or $g$ is zero, and Interlaces f g is the case $m = k + 1$ alone.

References

Steve Fisk, “Polynomials, roots, and interlacing,” arXiv:math/0612833 (2006). See also the interlacing overview on symmetricfunctions.com.

Definitions

Interlacing f ≪ g

RealRooted.StrictInterlsource

def StrictInterl (f g : ℝ[X]) : Prop := (f ≠ 0 ∧ f.Splits) ∧ (g ≠ 0 ∧ g.Splits) ∧
  ∃ (ss rs : List ℝ),
    ss.Pairwise (· ≤ ·) ∧ rs.Pairwise (· ≤ ·) ∧
    (↑ss : Multiset ℝ) = f.roots ∧ (↑rs : Multiset ℝ) = g.roots ∧
    ((ss.length + 1 = rs.length ∧ ListInterlaces ss rs) ∨
      (ss.length = rs.length ∧ ListAlternates ss rs))

Interlacing, allowing zero polynomials

RealRooted.Interlsource

def Interl (f g : ℝ[X]) : Prop :=
  f = 0 ∨ g = 0 ∨ StrictInterl f g

Interlacing with degrees differing by one

RealRooted.Interlacessource

def Interlaces (g f : ℝ[X]) : Prop := (f ≠ 0 ∧ f.Splits) ∧ (g ≠ 0 ∧ g.Splits) ∧
  g.natDegree + 1 = f.natDegree ∧
  ∃ (rs ss : List ℝ),
    rs.Pairwise (· ≤ ·) ∧ ss.Pairwise (· ≤ ·) ∧
    (↑rs : Multiset ℝ) = f.roots ∧
    (↑ss : Multiset ℝ) = g.roots ∧
    ListInterlaces ss rs

Polynomial interlacing

References

≔ Definitions

Definitions