Concepts

Common interleavers

A finite family of real-rooted polynomials $f_1, \dotsc, f_m$ has a common interleaver if a single real-rooted $h$ satisfies $f_i \ll h$ for every $i$. The family is compatible if every nonnegative combination $c_1 f_1 + \dotsb + c_m f_m$ is zero or real-rooted.

Theorem (Chudnovsky–Seymour). For real-rooted polynomials with positive leading coefficients, the following are equivalent:

  1. every pair is compatible;
  2. every pair has a common interleaver;
  3. the whole family has a common interleaver;
  4. the whole family is compatible.

The library proves each implication:

This is the interlacing input for the real-rootedness of independence polynomials of claw-free graphs; see the Chudnovsky–Seymour page.

References

M. Chudnovsky and P. Seymour, “The roots of the independence polynomial of a clawfree graph,” J. Combin. Theory Ser. B 97 (2007), 350–357. P. Brändén, “Unimodality, log-concavity, real-rootedness and beyond,” in Handbook of Enumerative Combinatorics, CRC Press (2015), Section 7.8.

Definitions

  • Common interleaver of a family

    RealRooted.HasCommonInterleaversource
    def HasCommonInterleaver (fs : List ℝ[X]) : Prop :=
  ∃ h : ℝ[X], ∀ f ∈ fs, StrictInterl f h

  • Pairwise common interleavers

    RealRooted.PairwiseHasCommonInterleaversource
    def PairwiseHasCommonInterleaver (fs : List ℝ[X]) : Prop :=
  ∀ (i j : Fin fs.length), i < j →
    ∃ h : ℝ[X], StrictInterl (fs.get i) h ∧ StrictInterl (fs.get j) h

  • Compatible pair

    RealRooted.Compatiblesource
    def Compatible (f g : ℝ[X]) : Prop :=
  ∀ α β : ℝ, 0 ≤ α → 0 ≤ β →
    C α * f + C β * g = 0 ∨
      ((C α * f + C β * g) ≠ 0 ∧ (C α * f + C β * g).Splits)

  • Compatible family

    RealRooted.FamilyCompatiblesource
    def FamilyCompatible (fs : List ℝ[X]) : Prop :=
  ∀ l : List (ℝ × ℝ[X]),
    (∀ ap ∈ l, ap.2 ∈ fs) →
    (∀ ap ∈ l, 0 ≤ ap.1) →
    weightedSum l = 0 ∨ ((weightedSum l) ≠ 0 ∧ (weightedSum l).Splits)

Theorems

  • Pairwise common interleavers give a common interleaver

    RealRooted.hasCommonInterleaver_of_pairwiseHasCommonInterleaversource
    theorem hasCommonInterleaver_of_pairwiseHasCommonInterleaver
    {fs : List ℝ[X]}
    (hrr : ∀ f ∈ fs, f.Splits)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
    (hpair : PairwiseHasCommonInterleaver fs) :
    HasCommonInterleaver fs

  • A family with a common interleaver has a real-rooted sum

    RealRooted.isRealRooted_sum_of_commonInterleaversource
    theorem isRealRooted_sum_of_commonInterleaver
    {fs : List ℝ[X]}
    (hcommon : HasCommonInterleaver fs)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
    (hne : fs ≠ []) : (fs.sum ≠ 0 ∧ fs.sum.Splits)

  • Pairwise common interleavers give a real-rooted sum

    RealRooted.isRealRooted_sum_of_pairwiseHasCommonInterleaversource
    theorem isRealRooted_sum_of_pairwiseHasCommonInterleaver
    {fs : List ℝ[X]}
    (hsplits : ∀ f ∈ fs, f.Splits)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f)
    (hpair : PairwiseHasCommonInterleaver fs)
    (hne : fs ≠ []) :
    fs.sum ≠ 0 ∧ fs.sum.Splits

  • A common interleaver gives a compatible family

    RealRooted.familyCompatible_of_commonInterleaversource
    theorem familyCompatible_of_commonInterleaver
    {fs : List ℝ[X]}
    (hcommon : HasCommonInterleaver fs)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
    FamilyCompatible fs

  • Pairwise common interleavers give pairwise compatibility

    RealRooted.pairwiseCompatible_of_pairwiseHasCommonInterleaversource
    theorem pairwiseCompatible_of_pairwiseHasCommonInterleaver
    {fs : List ℝ[X]}
    (hpair : PairwiseHasCommonInterleaver fs)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
    PairwiseCompatible fs

  • Chudnovsky–Seymour: a compatible pair has a common interleaver

    RealRooted.Challenges.CommonInterleaver.compatiblePair_hasCommonInterleaversource
    theorem compatiblePair_hasCommonInterleaver {f g : ℝ[X]} (hf : HasPosLeadingCoeff f)
    (hg : HasPosLeadingCoeff g) (hfg : Compatible f g) :
    ∃ h : ℝ[X], StrictInterl f h ∧ StrictInterl g h

  • Chudnovsky–Seymour: pairwise compatible ⇔ common interleaverMain result

    RealRooted.chudnovskySeymour_pairwiseCompatible_iff_commonInterleaversource
    theorem chudnovskySeymour_pairwiseCompatible_iff_commonInterleaver
    {fs : List ℝ[X]}
    (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
    PairwiseCompatible fs ↔ HasCommonInterleaver fs

  • Chudnovsky–Seymour: pairwise compatible ⇔ compatible familyMain result

    RealRooted.chudnovskySeymour_pairwiseCompatible_iff_familyCompatiblesource
    theorem chudnovskySeymour_pairwiseCompatible_iff_familyCompatible
    {fs : List ℝ[X]}
    (hrr : ∀ f ∈ fs, f ≠ 0 ∧ f.Splits)
    (hpos : ∀ f ∈ fs, HasPosLeadingCoeff f) :
    PairwiseCompatible fs ↔ FamilyCompatible fs

Lean source RealRooted/Challenges/CommonInterleaver.lean at revision 4b488d3c.