Reference catalog
Real-rooted polynomials
Definitions and theorems on real-rooted polynomials, interlacing and total positivity, formalized in Lean. Each statement links to its Lean source.
Concepts and families
Concepts and polynomial families, with the number of definitions (≔) and theorems (⊢) on each page.
- Concept 4 definitions 8 theoremsCommon interleaversMain results: Chudnovsky–Seymour: pairwise compatible ⇔ common interleaver; Chudnovsky–Seymour: pairwise compatible ⇔ compatible familyChudnovsky & Seymour · 2007
- Family 2 definitions 4 theoremsEulerian polynomialsMain results: Eulerian polynomials are real-rooted; Type B Eulerian polynomials are real-rootedFrobenius & Brenti · 1910–1994
- Family 1 definition 6 theoremsGeneralized Laguerre polynomialsMain results: Generalized Laguerre polynomials are real-rooted
- Family 2 definitions 3 theoremsGeneralized Narayana polynomialsMain results: Generalized Narayana polynomials are real-rooted; The Narayana transform preserves Pólya-frequency polynomialsMao, Wang, Dominici, Johnston & Jordaan · 2013–2026
- Family 5 definitions 9 theoremsGeneralized snake posetsMain results: Braun–Jal, Theorem 3.5: the snake recurrence; Braun–Jal, Theorem 4.1: snake polynomials are real-rooted and interlaceBraun & Jal · 2026
- Family 2 definitions 6 theoremsHermite polynomialsMain results: Hermite polynomials are real-rooted
- Concept 6 definitions 10 theoremsMultiplier sequencesMain results: Pólya–Schur: multiplier sequences via Jensen polynomials; Pólya–Schur: PF multiplier sequences are the Laguerre–Pólya type I class; …Pólya & Schur · 1914
- Family 4 definitions 5 theoremsParking functionsMain results: Parking function descent polynomials are real-rooted; Tieless parking function descent polynomials are real-rooted; …
- Concept 3 definitionsPolynomial interlacingFisk · 2006
Theorems
Theorem pages, and the main results from the concept and family pages. The complete list is under All results.
- Theorem 1 definition 2 theoremsAissen–Schoenberg–WhitneyAissen, Schoenberg & Whitney · 1952
- Theorem 4 definitions 3 theoremsBorcea–Brändén finite-symbol theoremsBorcea & Brändén · 2009
- TheoremBraun–Jal, Theorem 3.5: the snake recurrencefrom Generalized snake posetsBraun & Jal · 2026
- TheoremBraun–Jal, Theorem 4.1: snake polynomials are real-rooted and interlacefrom Generalized snake posetsBraun & Jal · 2026
- Theorem 1 definition 1 theoremBrändén–Solus symmetric decompositionBrändén & Solus · 2019
- Theorem 2 theoremsCauchy interlacingFisk · 2005
- Theorem 4 definitions 8 theoremsChow polynomials of totally nonnegative matricesBrändén & Vecchi · 2025
- TheoremChudnovsky–Seymour: pairwise compatible ⇔ common interleaverfrom Common interleaversChudnovsky & Seymour · 2007
- TheoremChudnovsky–Seymour: pairwise compatible ⇔ compatible familyfrom Common interleaversChudnovsky & Seymour · 2007
- Theorem 2 definitions 1 theoremClaw-free independence polynomialsChudnovsky & Seymour · 2007
- Theorem 2 definitions 2 theoremsDescartes' rule of signsDescartes · 1637
- TheoremEulerian polynomials are real-rootedfrom Eulerian polynomialsFrobenius & Brenti · 1910–1994
- Theorem 1 definition 2 theoremsFavard recurrencesFavard · 1935
- TheoremGeneralized Laguerre polynomials are real-rootedfrom Generalized Laguerre polynomials
- TheoremGeneralized Narayana polynomials are real-rootedfrom Generalized Narayana polynomialsMao, Wang, Dominici, Johnston & Jordaan · 2013–2026
- Theorem 5 definitions 8 theoremsHadamard products and Schur–Szegő compositionMaló, Pólya, Schur, Wagner & Garloff · 1895–1996
- TheoremHermite polynomials are real-rootedfrom Hermite polynomials
- Theorem 3 theoremsHermite–Biehler and Hurwitz criteriaHoltz · 2003
- Theorem 1 definition 1 theoremHermite–Poulain theoremHermite & Poulain
- Theorem 1 definition 1 theoremInterlacing from a monomial chain
- Theorem 2 definitions 1 theoremKurtz’s coefficient criterionKurtz · 1992
- TheoremLaguerre's theorem: φ(0), φ(1), … is a multiplier sequencefrom Multiplier sequencesPólya & Schur · 1914
- Theorem 4 definitions 5 theoremsLindström–Gessel–Viennot and total positivityLindström, Gessel & Viennot · 1973–1985
- Theorem 3 definitions 4 theoremsLiu's opposite-sign compatibility theoremLiu · 2012
- Theorem 3 definitions 2 theoremsMatrices preserving interlacing sequencesFisk & Brändén · 2006–2015
- Theorem 2 definitions 3 theoremsObreschkoff’s theoremObreschkoff & Dedieu · 1963–1992
- Theorem 2 definitions 1 theoremOperators preserving interlacingBrändén · 2011
- TheoremParking function descent polynomials are real-rootedfrom Parking functions
- TheoremParking function weak left peak polynomials are real-rootedfrom Parking functions
- Theorem 1 definition 5 theoremsPerron–Frobenius theoremPerron & Frobenius · 1907–1912
- TheoremPólya–Schur: classification of all multiplier sequencesfrom Multiplier sequencesPólya & Schur · 1914
- TheoremPólya–Schur: multiplier sequences via Jensen polynomialsfrom Multiplier sequencesPólya & Schur · 1914
- TheoremPólya–Schur: PF multiplier sequences are the Laguerre–Pólya type I classfrom Multiplier sequencesPólya & Schur · 1914
- Theorem 3 definitions 6 theoremsReal-rooted Eulerian variationsAlexandersson · 2026
- Theorem 3 definitions 4 theoremsRook polynomialsNijenhuis · 1976
- Theorem 3 definitions 3 theoremsSame-phase stability for graph polynomialsLeake & Ryder · 2019
- Theorem 3 definitions 2 theoremsSturm root countingSturm · 1829
- Theorem 2 definitions 8 theoremsThe binary-run transformation
- TheoremThe Narayana transform preserves Pólya-frequency polynomialsfrom Generalized Narayana polynomialsMao, Wang, Dominici, Johnston & Jordaan · 2013–2026
- TheoremTieless parking function descent polynomials are real-rootedfrom Parking functions
- Theorem 2 definitions 3 theoremsToric g-contribution polynomialsXiao · 2026
- Theorem 4 definitions 11 theoremsTotally nonnegative matrices and chain polynomialsBrändén & Saud Leite · 2024
- TheoremType B Eulerian polynomials are real-rootedfrom Eulerian polynomialsFrobenius & Brenti · 1910–1994
- Theorem 1 definition 1 theoremVeronese sections
- Theorem 3 theoremsWagner’s lemmaWagner · 1992