Theorems

Obreschkoff’s theorem

Two interlacing polynomials generate a real-rooted pencil. Conversely, a real-rooted pencil with the stated degree hypotheses forces one of the two interlacing orientations.

References

N. Obreschkoff, Verteilung und Berechnung der Nullstellen reeller Polynome, VEB Deutscher Verlag der Wissenschaften, 1963; J.-P. Dedieu, “Obreschkoff’s theorem revisited,” Journal of Pure and Applied Algebra 81 (1992), 269–278. See the contextual statement on symmetricfunctions.com.

Definitions

  • Every real combination is real-rooted

    RealRooted.AllComboRealRootedsource
    def AllComboRealRooted (f g : ℝ[X]) : Prop :=
  ∀ α β : ℝ, (C α * f + C β * g).Splits

  • Positive leading coefficient

    RealRooted.HasPosLeadingCoeffsource
    def HasPosLeadingCoeff (p : ℝ[X]) : Prop := 0 < p.leadingCoeff

Theorems

  • Interlacing gives a real-rooted pencil

    RealRooted.Challenges.Obreschkoff.allCombinationsRealRooted_of_interlacessource
    theorem allCombinationsRealRooted_of_interlaces :
    ∀ {f g : ℝ[X]}, StrictInterl f g → AllComboRealRooted f g

  • A real-rooted pencil gives interlacing

    RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRootedsource
    theorem interlaces_or_reverse_of_allCombinationsRealRooted :
    ∀ {f g : ℝ[X]},
      (f ≠ 0 ∧ f.Splits) →
      (g ≠ 0 ∧ g.Splits) →
      AllComboRealRooted f g →
      f.natDegree + 1 = g.natDegree ∨ f.natDegree = g.natDegree →
      StrictInterl f g ∨ StrictInterl g f

  • The converse for positive leading coefficients

    RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRooted_posLeadingsource
    theorem interlaces_or_reverse_of_allCombinationsRealRooted_posLeading {f g : ℝ[X]}
    (hf_pos : HasPosLeadingCoeff f) (hf_splits : f.Splits)
    (hg_pos : HasPosLeadingCoeff g) (hg_splits : g.Splits)
    (hall : AllComboRealRooted f g)
    (hdeg : f.natDegree + 1 = g.natDegree ∨ f.natDegree = g.natDegree) :
    StrictInterl f g ∨ StrictInterl g f

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