Browse the catalog

All results

All 89 definitions and 147 theorems in the catalog.

Kind	Result	Page	Source
theorem	1/k! is a PF multiplier sequence`RealRooted.isPFMultiplierSequence_inv_factorial`	Multiplier sequences	source
definition	2 × 2 interlacing condition`RealRooted.Has2x2InterlacingProperty`	Matrices preserving interlacing sequences	source
definition	2 × 2 interlacing condition, allowing zeros`RealRooted.Has2x2InterlacingProperty0`	Matrices preserving interlacing sequences	source
theorem	A common interleaver gives a compatible family`RealRooted.familyCompatible_of_commonInterleaver`	Common interleavers	source
theorem	A family with a common interleaver has a real-rooted sum`RealRooted.isRealRooted_sum_of_commonInterleaver`	Common interleavers	source
definition	A polynomial matrix acting on a sequence`RealRooted.matPolyAction`	Matrices preserving interlacing sequences	source
theorem	A positive eigenvector belongs to the Perron root`Matrix.CollatzWielandt.eq_perron_root_of_positive_eigenvector`	Perron–Frobenius theorem	source
theorem	A real-rooted pencil gives interlacing`RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRooted`	Obreschkoff’s theorem	source
theorem	A stable symbol gives a real-rootedness preserver`RealRooted.BorceaBranden.finiteSymbol_preservesRealRootedUpTo`	Borcea–Brändén finite-symbol theorems	source
theorem	A Sturm test for real-rootedness`RealRooted.splits_iff_distinctSturmVariations_sub_eq_natDegree`	Sturm root counting	source
theorem	A sum of polynomials interlacing h interlaces h`RealRooted.Challenges.Wagner.commonRight_add`	Wagner’s lemma	source
theorem	A zero prefix of length three breaks real-rootedness`RealRooted.BrandenVecchi.chowPolynomial_three_zero_prefix_six_not_splits`	Chow polynomials of totally nonnegative matrices	source
definition	Algebraic symbol of an operator`RealRooted.BorceaBranden.finiteAlgebraicSymbol`	Borcea–Brändén finite-symbol theorems	source
definition	Auxiliary polynomials Gₙ`RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.auxiliaryG`	Generalized snake posets	source
definition	Binary-run basis polynomials`RealRooted.binaryRunPolynomial`	The binary-run transformation	source
definition	Binary-run transformation`RealRooted.binaryRunTransform`	The binary-run transformation	source
definition	Board of a generalized snake poset`RealRooted.GeneralizedSnakePosets.generalizedSnakeBoard`	Generalized snake posets	source
theorem	Braun–Jal, Lemma 3.4`RealRooted.GeneralizedSnakePosets.lemma34ModifiedNarayanaInterlacing_modified`	Generalized snake posets	source
theorem	Braun–Jal, Theorem 3.5: the snake recurrenceMain result`RealRooted.GeneralizedSnakePosets.generalizedSnakeTheorem35`	Generalized snake posets	source
theorem	Braun–Jal, Theorem 4.1: snake polynomials are real-rooted and interlaceMain result`RealRooted.GeneralizedSnakePosets.theorem41_generalizedSnakeRookModel`	Generalized snake posets	source
theorem	Brändén–Solus, Theorem 2.6`RealRooted.Challenges.BrandenSolus.theorem26`	Brändén–Solus symmetric decomposition	source
theorem	c_n interlaces d_n`RealRooted.BrandenVecchi.chowPolynomial_interl_chowDerangement_of_isTotallyNonneg`	Chow polynomials of totally nonnegative matrices	source
definition	Chain polynomials`RealRooted.BrandenLeite.chainPolynomial`	Totally nonnegative matrices and chain polynomials	source
theorem	Chain polynomials have nonnegative coefficients`RealRooted.BrandenLeite.chainPolynomial_hasNonnegCoeffs_of_isTotallyNonneg`	Totally nonnegative matrices and chain polynomials	source
theorem	Characteristic polynomials of a principal submatrix interlace`RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_charpoly_interlaces`	Cauchy interlacing	source
definition	Chow derangement polynomials`RealRooted.BrandenVecchi.chowDerangement`	Chow polynomials of totally nonnegative matrices	source
theorem	Chow polynomials are real-rooted`RealRooted.BrandenVecchi.chowPolynomial_eq_zero_or_splits_of_isTotallyNonneg`	Chow polynomials of totally nonnegative matrices	source
theorem	Chow polynomials as signed-word enumerators`RealRooted.BrandenVecchi.finiteSupersymmetricChow_eq_finiteSignedWordEnumerator`	Chow polynomials of totally nonnegative matrices	source
theorem	Chow polynomials have nonnegative coefficients`RealRooted.BrandenVecchi.chowPolynomial_nonnegCoeffs_of_isTotallyNonneg`	Chow polynomials of totally nonnegative matrices	source
definition	Chow polynomials of a lower-triangular matrix`RealRooted.BrandenVecchi.chowPolynomial`	Chow polynomials of totally nonnegative matrices	source
definition	Chow polynomials of a Pólya frequency symbol`RealRooted.BrandenVecchi.aswEdreiChow`	Chow polynomials of totally nonnegative matrices	source
definition	Chow polynomials of a supersymmetric symbol`RealRooted.BrandenVecchi.finiteSupersymmetricChow`	Chow polynomials of totally nonnegative matrices	source
theorem	Chudnovsky–Seymour via Leake–Ryder`RealRooted.Graph.ClawFree.indepPoly_splits_of_leakeRyder`	Same-phase stability for graph polynomials	source
theorem	Chudnovsky–Seymour: a compatible pair has a common interleaver`RealRooted.chudnovskySeymour_compatiblePairHasCommonInterleaver`	Common interleavers	source
theorem	Chudnovsky–Seymour: claw-free graphs have real-rooted independence polynomials`RealRooted.Challenges.ChudnovskySeymour.clawFree_indepPoly_splits`	Claw-free independence polynomials	source
theorem	Chudnovsky–Seymour: pairwise compatible ⇔ common interleaverMain result`RealRooted.chudnovskySeymour_pairwiseCompatible_iff_commonInterleaver_of_pairBridge`	Common interleavers	source
theorem	Chudnovsky–Seymour: pairwise compatible ⇔ compatible familyMain result`RealRooted.chudnovskySeymour_pairwiseCompatible_iff_familyCompatible`	Common interleavers	source
theorem	Classification of stability preservers on a degree box`RealRooted.BorceaBranden.finiteComplexSymbolClassification`	Borcea–Brändén finite-symbol theorems	source
definition	Claw-free graph`RealRooted.Graph.ClawFree`	Claw-free independence polynomials	source
theorem	Column recurrence for the auxiliary polynomials Gₙ`RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.narayanaAuxiliaryGRecurrence_modified`	Generalized snake posets	source
definition	Common interleaver of a family`RealRooted.HasCommonInterleaver`	Common interleavers	source
definition	Compatible family`RealRooted.FamilyCompatible`	Common interleavers	source
definition	Compatible pair`RealRooted.Compatible`	Common interleavers	source
theorem	Consecutive chain polynomials interlace`RealRooted.BrandenLeite.interl_chainPolynomial_succ_of_isTotallyNonneg`	Totally nonnegative matrices and chain polynomials	source
theorem	Consecutive Chow polynomials interlace`RealRooted.BrandenVecchi.chowPolynomial_interl_succ_of_isTotallyNonneg`	Chow polynomials of totally nonnegative matrices	source
theorem	Consecutive Eulerian polynomials interlace`RealRooted.Challenges.Eulerian.interlaces_succ`	Eulerian polynomials	source
theorem	Consecutive generalized Laguerre polynomials interlace`RealRooted.generalizedLaguerre_strictInterl_succ`	Generalized Laguerre polynomials	source
theorem	Consecutive Hermite polynomials interlace`RealRooted.hermiteReal_strictInterl_succ`	Hermite polynomials	source
theorem	Consecutive modified Narayana polynomials interlace`RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomial_strictInterl_succ`	Generalized snake posets	source
theorem	Consecutive polynomials interlace`RealRooted.Challenges.Favard.interlacing`	Favard recurrences	source
theorem	Consecutive ternary run polynomials interlace`RealRooted.Applications.EulerianVariations.ternaryRunPolynomial_strictInterl`	Real-rooted Eulerian variations	source
theorem	Consecutive type B Eulerian polynomials interlace`RealRooted.Challenges.Eulerian.typeB_interlaces_succ`	Eulerian polynomials	source
theorem	Constant words give modified Narayana polynomials`RealRooted.GeneralizedSnakePosets.generalizedSnakeRookModel_snakePolynomial_of_isConstant`	Generalized snake posets	source
definition	Cyclic path descent polynomial`RealRooted.Applications.EulerianVariations.cyclicPathDescentPolynomial`	Real-rooted Eulerian variations	source
theorem	Cyclic path descents via the Narayana derivative`RealRooted.Applications.EulerianVariations.cyclicPathDescentPolynomial_eq_derivative`	Real-rooted Eulerian variations	source
theorem	Descartes' rule of signs`Polynomial.descartes_rule_of_signs`	Descartes' rule of signs	source
theorem	Descartes' rule of signs for negative roots`Polynomial.descartes_rule_of_signs_negative`	Descartes' rule of signs	source
definition	Descent polynomial of parking functions`RealRooted.ParkingFunctions.parkingDescentPolynomial`	Parking functions	source
definition	Descent polynomial of tieless parking functions`RealRooted.ParkingFunctions.tielessParkingDescentPolynomial`	Parking functions	source
definition	Diagonal operator of a sequence`RealRooted.diagonalOperator`	Multiplier sequences	source
definition	Edge-variable matching polynomial`RealRooted.Graph.multivariateMatchingPolynomialByEdges`	Same-phase stability for graph polynomials	source
theorem	Eigenvalues of a principal submatrix interlace`RealRooted.Challenges.CauchyInterlacing.principalSubmatrix_eigenvalues_interlace`	Cauchy interlacing	source
definition	Eulerian polynomials`RealRooted.eulerianTilde`	Eulerian polynomials	source
theorem	Eulerian polynomials are real-rootedMain result`RealRooted.Challenges.Eulerian.realRooted`	Eulerian polynomials	source
theorem	Every multiplier sequence is a PF one up to signs`RealRooted.IsMultiplierSequence.exists_pf_sign_normalization`	Multiplier sequences	source
definition	Every real combination is real-rooted`RealRooted.AllComboRealRooted`	Obreschkoff’s theorem	source
definition	Factorial Schur product`RealRooted.gwSchurProduct`	Hadamard products and Schur–Szegő composition	source
theorem	Favard polynomials are real-rooted`RealRooted.Challenges.Favard.realRooted`	Favard recurrences	source
definition	Favard three-term recurrence`RealRooted.SatisfiesFavardRecurrence`	Favard recurrences	source
definition	Finite multiplier sequence`RealRooted.IsFiniteMultiplierSequence`	Multiplier sequences	source
theorem	Finite Pólya–Schur theorem`RealRooted.Challenges.Hadamard.finitePolyaSchur_nonneg`	Hadamard products and Schur–Szegő composition	source
theorem	Finite-symbol theorem for real-rootedness preservers`RealRooted.BorceaBranden.finiteSymbolTheorem`	Borcea–Brändén finite-symbol theorems	source
theorem	Full truncated staircases have rook polynomial Pₙ`RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.truncatedStaircaseRookPolynomial_full_eq_modifiedNarayanaPolynomial`	Generalized snake posets	source
theorem	Garloff–Wagner, Theorem 12: the Schur product preserves interlacing`RealRooted.gwSchurProductInterl`	Hadamard products and Schur–Szegő composition	source
theorem	Garloff–Wagner: Hadamard products of PF polynomials are PF`RealRooted.gwHadamardProductPF`	Hadamard products and Schur–Szegő composition	source
theorem	Garloff–Wagner: Hadamard products preserve interlacing`RealRooted.gwHadamardProductInterl_of_strictInterl`	Hadamard products and Schur–Szegő composition	source
definition	Gaussian weight`RealRooted.hermiteGaussianWeight`	Hermite polynomials	source
definition	Generalized Laguerre polynomials`Polynomial.generalizedLaguerre`	Generalized Laguerre polynomials	source
theorem	Generalized Laguerre polynomials are orthogonal on the half-line`RealRooted.generalizedLaguerre_integral_orthogonal`	Generalized Laguerre polynomials	source
theorem	Generalized Laguerre polynomials are real-rootedMain result`RealRooted.generalizedLaguerre_splits`	Generalized Laguerre polynomials	source
theorem	Generalized Laguerre polynomials have negative roots for α > -1`RealRooted.generalizedLaguerre_roots_neg`	Generalized Laguerre polynomials	source
theorem	Generalized Laguerre polynomials have simple roots`RealRooted.generalizedLaguerre_hasSimpleRoots`	Generalized Laguerre polynomials	source
theorem	Generalized Laguerre polynomials satisfy a Favard recurrence`RealRooted.generalizedLaguerre_satisfiesFavardRecurrence`	Generalized Laguerre polynomials	source
definition	Generalized Narayana polynomials`RealRooted.narayanaPolynomial`	Generalized Narayana polynomials	source
theorem	Generalized Narayana polynomials are Pólya-frequency`RealRooted.narayanaPolynomialRootLocation`	Generalized Narayana polynomials	source
theorem	Generalized Narayana polynomials are real-rootedMain result`RealRooted.splits_narayanaPolynomial`	Generalized Narayana polynomials	source
definition	Hadamard product`RealRooted.hadamardProduct`	Hadamard products and Schur–Szegő composition	source
theorem	Hadamard products preserve interlacing`RealRooted.Challenges.Hadamard.garloffWagnerHadamardNonnegInterl`	Hadamard products and Schur–Szegő composition	source
theorem	Hermite polynomials are orthogonal for the Gaussian weight`RealRooted.hermiteReal_integral_orthogonal`	Hermite polynomials	source
theorem	Hermite polynomials are real-rootedMain result`RealRooted.hermiteReal_isRealRooted`	Hermite polynomials	source
theorem	Hermite polynomials form a Sturm sequence`RealRooted.hermiteReal_isSturmSeq`	Hermite polynomials	source
theorem	Hermite polynomials have simple roots`RealRooted.hermiteReal_hasSimpleRoots`	Hermite polynomials	source
theorem	Hermite polynomials satisfy a Favard recurrence`RealRooted.hermiteReal_satisfiesFavardRecurrence`	Hermite polynomials	source
theorem	Hermite–Biehler: interlacing gives stability`RealRooted.Challenges.HermiteBiehlerHurwitz.hermiteBiehler_forward`	Hermite–Biehler and Hurwitz criteria	source
theorem	Hermite–Biehler: stability gives interlacing`RealRooted.Challenges.HermiteBiehlerHurwitz.hermiteBiehler_converse`	Hermite–Biehler and Hurwitz criteria	source
theorem	Hermite–Poulain theorem`RealRooted.HermitePoulain.differential_operator_preserves_real_rooted`	Hermite–Poulain theorem	source
theorem	Hurwitz criterion via total nonnegativity`RealRooted.Challenges.HermiteBiehlerHurwitz.classicalHurwitzCriterion`	Hermite–Biehler and Hurwitz criteria	source
definition	Hypergeometric polynomials R_d`RealRooted.ParkingFunctions.ToricContribution.rPolynomial`	Toric g-contribution polynomials	source
definition	Independence polynomial`RealRooted.Graph.indepPoly`	Claw-free independence polynomials	source
definition	Index set of a Toeplitz minor`RealRooted.StrictToeplitzMinorIndex`	Lindström–Gessel–Viennot and total positivity	source
theorem	Interlacing across lengths`RealRooted.strictInterl_binaryRunTransform_succ`	The binary-run transformation	source
definition	Interlacing f ≪ g`RealRooted.StrictInterl`	Polynomial interlacing	source
theorem	Interlacing gives a real-rooted pencil`RealRooted.Challenges.Obreschkoff.allCombinationsRealRooted_of_interlaces`	Obreschkoff’s theorem	source
definition	Interlacing preserver, up to orientation`RealRooted.PreservesInterlacingPairsUpToOrder0`	Operators preserving interlacing	source
definition	Interlacing with degrees differing by one`RealRooted.Interlaces`	Polynomial interlacing	source
definition	Interlacing, allowing zero polynomials`RealRooted.Interl`	Polynomial interlacing	source
theorem	Irreducible matrices have a positive eigenvector`Matrix.exists_positive_eigenvector_of_irreducible`	Perron–Frobenius theorem	source
definition	Jensen polynomials`RealRooted.jensenPolynomial`	Multiplier sequences	source
theorem	k + r is a PF multiplier sequence for r ≥ 0`RealRooted.isPFMultiplierSequence_natCast_add`	Multiplier sequences	source
definition	Kurtz inequalities a_k² > 4 a_{k-1} a_{k+1}`RealRooted.Kurtz.KurtzStrictInequalities`	Kurtz’s coefficient criterion	source
theorem	Kurtz's criterion`RealRooted.Kurtz.coefficient_criterion`	Kurtz’s coefficient criterion	source
theorem	Laguerre's theorem: φ(0), φ(1), … is a multiplier sequenceMain result`RealRooted.isMultiplierSequence_eval_of_roots_nonpos`	Multiplier sequences	source
definition	Laguerre–Pólya class of type I`RealRooted.IsLaguerrePolyaTypeI`	Multiplier sequences	source
theorem	Leake–Ryder: same-phase stable if and only if claw-free`RealRooted.Graph.multivariateIndepPoly_samePhaseStable_iff_clawFree`	Same-phase stability for graph polynomials	source
definition	Letters L and R of a snake word`RealRooted.GeneralizedSnakePosets.SnakeLetter`	Generalized snake posets	source
theorem	Liu, Corollary 2.2: degrees differ by at most two`RealRooted.LiuOppositeSigns.corollary22DegreeDiff_proof`	Liu's opposite-sign compatibility theorem	source
theorem	Liu, Theorem 2.1 (corrected)`RealRooted.LiuOppositeSigns.compatible_iff_theorem21RootCountBranchesWithCommon_nonconstant`	Liu's opposite-sign compatibility theorem	source
definition	Lower-bidiagonal chip`RealRooted.LGV.ChipNetwork.Chip`	Lindström–Gessel–Viennot and total positivity	source
theorem	Maló: Hadamard products of totally nonnegative Toeplitz matrices`RealRooted.Challenges.Hadamard.maloToeplitzHadamard`	Hadamard products and Schur–Szegő composition	source
definition	Matrix of a word of chips`RealRooted.LGV.ChipNetwork.wordMatrix`	Lindström–Gessel–Viennot and total positivity	source
theorem	Modified Narayana polynomials are Pólya-frequency`RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomial_isPFPolynomial`	Generalized snake posets	source
definition	Modified Narayana polynomials Pₙ`RealRooted.GeneralizedSnakePosets.modifiedNarayanaPolynomial`	Generalized snake posets	source
definition	Monomial-chain condition`RealRooted.PreservesPFShiftInterlacingOnDegree`	Interlacing from a monomial chain	source
theorem	Monotonicity in α`RealRooted.motzkinWeightedRow_inv_ascPochhammer_succ_strictInterl`	The binary-run transformation	source
theorem	Motzkin-ascent polynomials (A114580) form a Sturm chain`RealRooted.motzkinAscentRow_strictInterl_succ`	The binary-run transformation	source
theorem	Multiplication by x reverses interlacing`RealRooted.Challenges.Wagner.mulX_iff`	Wagner’s lemma	source
definition	Multiplier sequence`RealRooted.IsMultiplierSequence`	Multiplier sequences	source
definition	Multivariate independence polynomial`RealRooted.Graph.multivariateIndepPoly`	Same-phase stability for graph polynomials	source
definition	Multivariate peak-value polynomial`RealRooted.peakValuePolynomial`	Real-rooted Eulerian variations	source
definition	Narayana transform`RealRooted.narayanaTransform`	Generalized Narayana polynomials	source
definition	Nijenhuis's signed rook polynomial`RealRooted.Rook.nijenhuisRookPolynomial`	Rook polynomials	source
definition	Non-nesting rook polynomial of a board`RealRooted.GeneralizedSnakePosets.FiniteSkewBoard.rookPolynomial`	Generalized snake posets	source
definition	Number of distinct roots in an interval`RealRooted.distinctRootCountIoo`	Sturm root counting	source
definition	Number of negative roots`Polynomial.negativeRootCount`	Descartes' rule of signs	source
definition	Number of positive roots`Polynomial.positiveRootCount`	Descartes' rule of signs	source
definition	Number of roots in [x, ∞)`RealRooted.LiuOppositeSigns.rootCountAtOrAbove`	Liu's opposite-sign compatibility theorem	source
definition	Opposite leading signs`RealRooted.LiuOppositeSigns.OppositeLeadingSigns`	Liu's opposite-sign compatibility theorem	source
definition	Pairwise common interleavers`RealRooted.PairwiseHasCommonInterleaver`	Common interleavers	source
theorem	Pairwise common interleavers give a common interleaver`RealRooted.hasCommonInterleaver_of_pairwiseHasCommonInterleaver`	Common interleavers	source
theorem	Pairwise common interleavers give a real-rooted sum`RealRooted.isRealRooted_sum_of_pairwiseHasCommonInterleaver`	Common interleavers	source
theorem	Pairwise common interleavers give pairwise compatibility`RealRooted.pairwiseCompatible_of_pairwiseHasCommonInterleaver`	Common interleavers	source
theorem	Parking function descent polynomials are real-rootedMain result`RealRooted.ParkingFunctions.parkingDescentPolynomial_splits`	Parking functions	source
theorem	Parking function weak left peak polynomials are real-rootedMain result`RealRooted.ParkingFunctions.map_parkingWeakLeftPeakPolynomialInt_splits`	Parking functions	source
definition	Parking functions`RealRooted.ParkingFunctions.IsParkingFunction`	Parking functions	source
theorem	Path networks give Pólya frequency sequences`RealRooted.isPolyaFreqSeq_of_minorOrderedCertificates`	Lindström–Gessel–Viennot and total positivity	source
theorem	Path networks give totally nonnegative matrices`LGV.FinitePathNetwork.matrix_isTotallyNonneg_of_orderedCertificates`	Lindström–Gessel–Viennot and total positivity	source
theorem	Paths of length n and powers of the edge matrix`Quiver.Path.sum_weight_exactLength_eq_edgeSumMatrix_pow`	Lindström–Gessel–Viennot and total positivity	source
definition	Perron root`Matrix.CollatzWielandt.perronRoot`	Perron–Frobenius theorem	source
theorem	PF coefficients give real nonpositive zeros`RealRooted.Challenges.AissenSchoenbergWhitney.forwardTheorem`	Aissen–Schoenberg–Whitney	source
definition	PF multiplier sequence`RealRooted.IsPFMultiplierSequence`	Multiplier sequences	source
theorem	PF multiplier sequences are log-concave`RealRooted.IsPFMultiplierSequence.logConcave`	Multiplier sequences	source
definition	PF polynomial`RealRooted.IsPFPolynomial`	Hadamard products and Schur–Szegő composition	source
theorem	Planar networks from Whitney elimination`RealRooted.BrandenLeite.networkMatrix_resolutionLambda_eq`	Totally nonnegative matrices and chain polynomials	source
theorem	Pollak's cyclic action: descents of parking functions and of words`RealRooted.ParkingFunctions.succ_nsmul_parkingDescentPolynomialInt_eq_literalWordDescentPolynomialInt`	Parking functions	source
definition	Positive coefficients`RealRooted.Kurtz.PositiveCoeffsUpToDegree`	Kurtz’s coefficient criterion	source
theorem	Positive constant diagonal`RealRooted.BrandenLeite.chainPolynomial_isPFPolynomial_of_pos_constantDiagonal`	Totally nonnegative matrices and chain polynomials	source
theorem	Positive constant term gives strictly negative zeros`RealRooted.Challenges.BinaryRunTransformation.preservesStrictlyNegativeRoots`	The binary-run transformation	source
definition	Positive leading coefficient`RealRooted.HasPosLeadingCoeff`	Obreschkoff’s theorem	source
theorem	Positive weighted sums are real-rooted`RealRooted.ParkingFunctions.ToricContribution.weightedNormalizedReversedContributionFamily_sum_splits`	Toric g-contribution polynomials	source
theorem	Primitive matrices: uniqueness of the eigenvector`Matrix.pft_primitive`	Perron–Frobenius theorem	source
definition	Probabilists' Hermite polynomials`RealRooted.hermiteReal`	Hermite polynomials	source
theorem	Products of polynomial value sequences are PF`RealRooted.Challenges.Hadamard.polynomialValueProductPolyaFrequency`	Hadamard products and Schur–Szegő composition	source
definition	Pólya frequency sequence`RealRooted.IsPolyaFreqSeq`	Aissen–Schoenberg–Whitney	source
theorem	Pólya frequency symbols give PF Chow polynomials`RealRooted.BrandenVecchi.aswEdreiFullProjectiveChow_theorem`	Chow polynomials of totally nonnegative matrices	source
theorem	Pólya–Schur: classification of all multiplier sequencesMain result`RealRooted.isMultiplierSequence_iff_isLaguerrePolyaTypeISigned_complexExpGeneratingFunction`	Multiplier sequences	source
theorem	Pólya–Schur: multiplier sequences via Jensen polynomialsMain result`RealRooted.isMultiplierSequence_iff_jensenPolynomial_isPF`	Multiplier sequences	source
theorem	Pólya–Schur: PF multiplier sequences are the Laguerre–Pólya type I classMain result`RealRooted.isPFMultiplierSequence_iff_isLaguerrePolyaTypeI_complexExpGeneratingFunction`	Multiplier sequences	source
definition	Rank-one operator with stable image`RealRooted.BorceaBranden.HasStableRankOneRepresentation`	Borcea–Brändén finite-symbol theorems	source
theorem	Real nonpositive zeros give PF coefficients`RealRooted.Challenges.AissenSchoenbergWhitney.reverseTheorem`	Aissen–Schoenberg–Whitney	source
definition	Real-rootedness preserver`RealRooted.PreservesRealRootedOrZero`	Operators preserving interlacing	source
definition	Real-rootedness preserver up to degree d`RealRooted.BorceaBranden.PreservesRealRootedUpTo`	Borcea–Brändén finite-symbol theorems	source
theorem	Real-rootedness preservers preserve interlacing`RealRooted.Challenges.OperatorPreservers.realRootedPreserver_preservesInterlacing`	Operators preserving interlacing	source
theorem	Reciprocal rising factorials 1/(α)ₖ form a PF multiplier sequence`RealRooted.isPFMultiplierSequence_inv_ascPochhammer`	Multiplier sequences	source
theorem	Repeated-chip kernel rows are PF polynomials`RealRooted.LGV.RepeatedChip.kernelRow_isPFPolynomial`	Lindström–Gessel–Viennot and total positivity	source
definition	Repeated-chip kernel sequence`RealRooted.LGV.RepeatedChip.kernelSequence`	Lindström–Gessel–Viennot and total positivity	source
theorem	Repeated-chip kernel sequences are PF`RealRooted.LGV.RepeatedChip.kernelSequence_isPolyaFreqSeq`	Lindström–Gessel–Viennot and total positivity	source
theorem	Resolvable if and only if totally nonnegative`RealRooted.BrandenLeite.isResolvable_iff_lowerUnitriangular_and_isTotallyNonneg`	Totally nonnegative matrices and chain polynomials	source
definition	Resolvable matrix`RealRooted.BrandenLeite.IsResolvable`	Totally nonnegative matrices and chain polynomials	source
definition	Rook placement`RealRooted.Rook.IsRookPlacement`	Rook polynomials	source
theorem	Rook polynomials are bipartite matching polynomials`RealRooted.Challenges.Nijenhuis.bipartiteMatchingIdentity`	Rook polynomials	source
theorem	Rook polynomials of boards are real-rooted`RealRooted.Challenges.Nijenhuis.ordinaryRealRooted`	Rook polynomials	source
definition	Root-count condition of the corrected Theorem 2.1`RealRooted.LiuOppositeSigns.theorem21RootCountBranchesWithCommon`	Liu's opposite-sign compatibility theorem	source
definition	Rows of 1 / (1 - x h(z))`RealRooted.BrandenLeite.compositionRow`	Totally nonnegative matrices and chain polynomials	source
theorem	Rows of 1 / (1 - x h(z)) are PF and interlace`RealRooted.BrandenLeite.compositionRows_mk_pf_and_interl_of_zero`	Totally nonnegative matrices and chain polynomials	source
theorem	Rows of 1 / (1 - x z (1+z)^d)`RealRooted.BrandenLeite.binomialCompositionRows_pf_and_interl`	Totally nonnegative matrices and chain polynomials	source
theorem	Rows of 1 / (1 - x z / (1-z)^e)`RealRooted.BrandenLeite.inversePowerCompositionRows_pf_and_interl`	Totally nonnegative matrices and chain polynomials	source
definition	Rows of g / (1 - x g h)`RealRooted.BrandenLeite.twoKernelRow`	Totally nonnegative matrices and chain polynomials	source
theorem	Rows of g / (1 - x g h) are PF and interlace`RealRooted.BrandenLeite.twoKernelRows_pf_and_interl`	Totally nonnegative matrices and chain polynomials	source
definition	Same-phase stability`RealRooted.SamePhaseStable`	Same-phase stability for graph polynomials	source
definition	Schur–Szegő composition`RealRooted.schurSzegoComp`	Hadamard products and Schur–Szegő composition	source
theorem	Schur–Szegő composition preserves real-rootedness`RealRooted.Challenges.Hadamard.finiteSchurSzegoComposition`	Hadamard products and Schur–Szegő composition	source
definition	Sign variations of the Sturm sequence`RealRooted.sturmVariations`	Sturm root counting	source
definition	Signed remainder sequence`Polynomial.signedRemainderSequence`	Sturm root counting	source
theorem	Specialization to Smirnov word polynomials`RealRooted.BrandenVecchi.finiteSupersymmetricChow_replicate_one_nil_eq_smirnov`	Chow polynomials of totally nonnegative matrices	source
definition	Stability preserver on a degree box`RealRooted.BorceaBranden.PreservesComplexStabilityOnDegreeBox`	Borcea–Brändén finite-symbol theorems	source
theorem	Sturm's theorem`RealRooted.distinctRootCountIoo_eq_distinctSturmVariations_sub`	Sturm root counting	source
theorem	Such matrices preserve interlacing sequences`RealRooted.Challenges.MatrixInterlacing.preserves_interlacing_sequences`	Matrices preserving interlacing sequences	source
definition	Symmetric I_d-decomposition`RealRooted.IsIdDecomposition`	Brändén–Solus symmetric decomposition	source
definition	Ternary run polynomial`RealRooted.Applications.EulerianVariations.ternaryRunPolynomial`	Real-rooted Eulerian variations	source
theorem	Ternary run polynomials are PF`RealRooted.Applications.EulerianVariations.ternaryRunPolynomial_isPF`	Real-rooted Eulerian variations	source
theorem	The common-left version`RealRooted.Challenges.Wagner.commonLeft_add`	Wagner’s lemma	source
theorem	The converse for positive leading coefficients`RealRooted.Challenges.Obreschkoff.interlaces_or_reverse_of_allCombinationsRealRooted_posLeading`	Obreschkoff’s theorem	source
theorem	The matching polynomial is same-phase stable`RealRooted.Graph.multivariateMatchingPolynomialByEdges_samePhaseStable`	Same-phase stability for graph polynomials	source
theorem	The monomial chain gives interlacing preservation`RealRooted.Challenges.MonomialChainOperator.preservesInterlacing`	Interlacing from a monomial chain	source
theorem	The Narayana transform preserves Pólya-frequency polynomialsMain result`RealRooted.narayanaTransformPreservesPF`	Generalized Narayana polynomials	source
definition	The operator f(D)`RealRooted.HermitePoulain.applyAsDifferentialOperator`	Hermite–Poulain theorem	source
theorem	The peak-value polynomial is real stable`RealRooted.Applications.EulerianVariations.peakValuePolynomial_stable`	Real-rooted Eulerian variations	source
theorem	The Perron root has a nonnegative eigenvector`Matrix.exists_nonneg_mulVec_eq_perronRoot_smul`	Perron–Frobenius theorem	source
theorem	The Perron root is the spectral radius`Matrix.perron_root_is_spectral_radius`	Perron–Frobenius theorem	source
theorem	The published Theorem 2.1 fails`RealRooted.LiuOppositeSigns.not_theorem21CompatibleToRootCountBranchesNonconstantStatement`	Liu's opposite-sign compatibility theorem	source
theorem	The R_d have a common interleaver`RealRooted.ParkingFunctions.ToricContribution.normalizedRPolynomialFamily_hasCommonLeftInterleaver`	Toric g-contribution polynomials	source
theorem	The same, allowing zero rows`RealRooted.Challenges.MatrixInterlacing.preserves_interlacing_sequences_zeroAware`	Matrices preserving interlacing sequences	source
theorem	The signed rook polynomial has nonnegative roots`RealRooted.Challenges.Nijenhuis.signedRoots_nonnegative`	Rook polynomials	source
theorem	The Sturm chain for γ_m = 1/(α)_m`RealRooted.motzkinWeightedRow_inv_ascPochhammer_strictInterl_succ`	The binary-run transformation	source
theorem	The transformation preserves interlacing`RealRooted.strictInterl_binaryRunTransform`	The binary-run transformation	source
theorem	The transformation preserves PF polynomials`RealRooted.Challenges.BinaryRunTransformation.preservesPF`	The binary-run transformation	source
theorem	Theorem 2.1 for pairs without common roots`RealRooted.LiuOppositeSigns.theorem21CompatibleRootCountNoCommonNonconstant`	Liu's opposite-sign compatibility theorem	source
theorem	Theorem 4.1 from the combinatorial inputs`RealRooted.GeneralizedSnakePosets.theorem41NonNestingRook_modified_of_sourceInputs`	Generalized snake posets	source
theorem	Tieless descents and a Brändén–Vecchi Chow polynomial`RealRooted.ParkingFunctions.succ_nsmul_tielessParkingDescentPolynomial_eq_chowPolynomial`	Parking functions	source
theorem	Tieless parking function descent polynomials are real-rootedMain result`RealRooted.ParkingFunctions.map_tielessParkingDescentPolynomial_splits`	Parking functions	source
theorem	Tiling polynomials of weighted lower shifts are PF`RealRooted.BrandenLeite.weightedShiftTilingRow_separated_isPFPolynomial`	Totally nonnegative matrices and chain polynomials	source
definition	Toeplitz matrix of a sequence`RealRooted.toeplitz`	Hadamard products and Schur–Szegő composition	source
definition	Toric g-contribution polynomial`RealRooted.ParkingFunctions.ToricContribution.toricContribution`	Toric g-contribution polynomials	source
definition	Type B Eulerian polynomials`RealRooted.typeBEulerian`	Eulerian polynomials	source
theorem	Type B Eulerian polynomials are real-rootedMain result`RealRooted.Challenges.Eulerian.typeB_realRooted`	Eulerian polynomials	source
theorem	Type I functions sampled at 0, 1, 2, … are PF multiplier sequences`RealRooted.IsLaguerrePolyaTypeI.isPFMultiplierSequence_eval_natCast`	Multiplier sequences	source
definition	Veronese section`RealRooted.veroneseSectionPolynomial`	Veronese sections	source
theorem	Veronese sections preserve real-rootedness`RealRooted.Challenges.VeroneseSections.preserve_realRooted_nonneg`	Veronese sections	source
definition	Weak left peak polynomial of parking functions`RealRooted.ParkingFunctions.parkingWeakLeftPeakPolynomialInt`	Parking functions	source
theorem	Weighted Motzkin rows form a Sturm chain`RealRooted.motzkinWeightedRow_strictInterl_succ`	The binary-run transformation	source
theorem	Weighted peak-value diagonals interlace`RealRooted.Applications.EulerianVariations.peakValueWeightedDiagonal_consecutive_strictInterl`	Real-rooted Eulerian variations	source
definition	Weighted rook polynomial`RealRooted.Rook.weightedRookPolynomial`	Rook polynomials	source
theorem	Weighted rook polynomials are real-rooted`RealRooted.Challenges.Nijenhuis.weightedRealRooted`	Rook polynomials	source
theorem	Xiao's Conjecture 4.2`RealRooted.ParkingFunctions.ToricContribution.toricContributionRow_isInterlacingSeq`	Toric g-contribution polynomials	source
theorem	Zeros of chain polynomials lie in [-1, 0]`RealRooted.BrandenLeite.roots_chainPolynomial_mem_Icc_of_isTotallyNonneg`	Totally nonnegative matrices and chain polynomials	source
theorem	Zeros of the cyclic path descent polynomial`RealRooted.Applications.EulerianVariations.cyclicPathDescentPolynomial_simple_root_description`	Real-rooted Eulerian variations	source