Theorems

Favard recurrences

A monic three-term recurrence with positive subdiagonal coefficients produces nonzero real-rooted polynomials. Consecutive polynomials interlace.

References

J. Favard, “Sur les polynômes de Tchebicheff,” Comptes rendus de l’Académie des sciences 200 (1935), 2052–2053. See also the interlacing overview on symmetricfunctions.com.

Definitions

  • Favard three-term recurrence

    RealRooted.SatisfiesFavardRecurrencesource
    def SatisfiesFavardRecurrence {R : Type*} [Ring R]
    (P : Nat → R[X]) (α β : Nat → R) : Prop :=
  P 0 = 1 ∧
  P 1 = X - C (α 0) ∧
  ∀ n : Nat,
    P (n + 2) =
      (X - C (α (n + 1))) * P (n + 1) - C (β (n + 1)) * P n

Theorems

  • Consecutive polynomials interlace

    RealRooted.Challenges.Favard.interlacingsource
    theorem interlacing :
    ∀ {P : Nat → ℝ[X]} {α β : Nat → ℝ},
      SatisfiesFavardRecurrence P α β →
      (∀ n : Nat, 0 < β (n + 1)) →
      ∀ n : Nat, StrictInterl (P n) (P (n + 1))

  • Favard polynomials are real-rooted

    RealRooted.Challenges.Favard.realRootedsource
    theorem realRooted :
    ∀ {P : Nat → ℝ[X]} {α β : Nat → ℝ},
      SatisfiesFavardRecurrence P α β →
      (∀ n : Nat, 0 < β (n + 1)) →
      ∀ n : Nat, (P n) ≠ 0 ∧ (P n).Splits

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