Theorems

Brändén–Solus symmetric decomposition

The $I_d$-decomposition writes a polynomial as $a + Xb$ with reciprocal symmetry conditions on $a$ and $b$. Under the hypotheses of Brändén–Solus Theorem 2.6, these two pieces interlace.

References

P. Brändén and L. Solus, “Symmetric decompositions and real-rootedness,” International Mathematics Research Notices 2021 (2021), 7764–7798. See the symmetric-decomposition overview on symmetricfunctions.com.

Definitions

  • Symmetric I_d-decomposition

    RealRooted.IsIdDecompositionsource
    def IsIdDecomposition (d : ℕ) (p a b : ℝ[X]) : Prop :=
  p = a + X * b ∧
  a.natDegree ≤ d ∧
  b.natDegree ≤ d - 1 ∧
  IdTransform d a = a ∧
  IdTransform (d - 1) b = b

Theorems

  • Brändén–Solus, Theorem 2.6

    RealRooted.Challenges.BrandenSolus.theorem26source
    theorem theorem26 :
    ∀ {d : ℕ} {p a b : ℝ[X]},
      p.natDegree ≤ d →
      IsIdDecomposition d p a b →
      HasNonnegCoeffs a →
      HasNonnegCoeffs b →
      a ≠ 0 →
      b ≠ 0 →
      (StrictInterl b a ↔ StrictInterl a p) ∧
      (StrictInterl a p ↔ StrictInterl b p) ∧
      (StrictInterl b p ↔ StrictInterl (IdTransform d p) p) ∧
      (StrictInterl (IdTransform d p) p ↔
        StrictInterl (RdTransform d (fPolynomial d p)) (fPolynomial d p))

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