Theorems

Wagner’s lemma

If $f$ and $g$ both interlace $h$, then $f + g$ interlaces $h$; the analogous common-left statement also holds. For polynomials with nonpositive roots, multiplication by $X$ reverses the interlacing orientation.

References

D. G. Wagner, “Total positivity of Hadamard products,” Journal of Mathematical Analysis and Applications 163 (1992), 459–483. See the contextual statement on symmetricfunctions.com.

Theorems

  • A sum of polynomials interlacing h interlaces h

    RealRooted.Challenges.Wagner.commonRight_addsource
    theorem commonRight_add {f g h : ℝ[X]}
    (hf : RealRooted.Wagner.HasNonposRootsPosLeading f)
    (hg : RealRooted.Wagner.HasNonposRootsPosLeading g)
    (hfh : StrictInterl f h) (hgh : StrictInterl g h) :
    StrictInterl (f + g) h

  • The common-left version

    RealRooted.Challenges.Wagner.commonLeft_addsource
    theorem commonLeft_add {f g h : ℝ[X]}
    (hf : RealRooted.Wagner.HasNonposRootsPosLeading f)
    (hg : RealRooted.Wagner.HasNonposRootsPosLeading g)
    (hhf : StrictInterl h f) (hhg : StrictInterl h g) :
    StrictInterl h (f + g)

  • Multiplication by x reverses interlacing

    RealRooted.Challenges.Wagner.mulX_iffsource
    theorem mulX_iff {f g : ℝ[X]}
    (hf : RealRooted.Wagner.HasNonposRootsPosLeading f)
    (hg : RealRooted.Wagner.HasNonposRootsPosLeading g)
    (hdeg : f.natDegree + 1 = g.natDegree) :
    StrictInterl f g ↔ StrictInterl g (X * f)

Lean source RealRooted/Challenges/Wagner.lean at revision 5827550b.