RealRooted.lean

import RealRooted.ASWCubicCharacteristic
import RealRooted.ASWCubicClosedForm
import RealRooted.ASWCubicClosedFormAdapter
import RealRooted.ASWCubicDegreeThree
import RealRooted.ASWCubicDominance
import RealRooted.ASWCubicEqualModulus
import RealRooted.ASWCubicMinors
import RealRooted.ASWCubicNonrealFactor
import RealRooted.ASWCubicRecurrence
import RealRooted.ASWKarlinKernel
import RealRooted.ASWKarlinMatrix
import RealRooted.ASWKarlinSineBounds
import RealRooted.ASWKarlinThreshold
import RealRooted.ASWKarlinVariation
import RealRooted.ASWKarlinVectors
import RealRooted.AffineDerivative
import RealRooted.AffineFamily
import RealRooted.AffineFamily.Basic
import RealRooted.AffineFamily.Boundary
import RealRooted.AffineFamily.LowDegree
import RealRooted.AffineFamily.PositiveFamily
import RealRooted.AffineFamily.RootCrossing
import RealRooted.AffineFamily.Wronskian
import RealRooted.AissenSchoenbergWhitney
import RealRooted.AissenSchoenbergWhitneyBase
import RealRooted.AllCombo
import RealRooted.Apolarity
import RealRooted.Analysis.PowerTail
import RealRooted.Analysis.PowerTail.Bernoulli
import RealRooted.Analysis.PowerTail.Quadratic
import RealRooted.Analysis.PowerTail.Telescoping
import RealRooted.ArrayPolynomialDeterminant
import RealRooted.ArrayPolynomialDeterminantIdentification
import RealRooted.ArrayPolynomialDeterminantRecurrence
import RealRooted.ArrayPolynomialSchur
import RealRooted.ArrayPolynomialWeights
import RealRooted.Basic
import RealRooted.Basic.AffineInterlacing
import RealRooted.Bezoutian
import RealRooted.BivariateOpenMapping
import RealRooted.BorceaBranden.Applications.AffineFiniteSymbol
import RealRooted.BorceaBranden.Applications.BidiagonalSymbol
import RealRooted.BorceaBranden.Applications.BidiagonalSymbol.RealConsequences
import RealRooted.BorceaBranden.Applications.ComplexClassification
import RealRooted.BorceaBranden.Applications.ComplexUnivariateSymbol
import RealRooted.BorceaBranden.Applications.DegreeBoxPolarization
import RealRooted.BorceaBranden.Applications.EulerFiniteSymbol
import RealRooted.BorceaBranden.Applications.GeneralDegreeBoxPolarization
import RealRooted.BorceaBranden.Applications.HomogenizeStable
import RealRooted.BorceaBranden.Applications.RealUnivariateSymbol
import RealRooted.BorceaBranden.Applications.RealUnivariateSymbol.Interlacing
import RealRooted.BorceaBranden.Applications.UnivariateSymbol
import RealRooted.BorceaBranden.BoundarySpecialization
import RealRooted.BorceaBranden.FiniteSymbolBasis
import RealRooted.BorceaBranden.FiniteSymbolClassification
import RealRooted.BorceaBranden.FiniteSymbolCoefficient
import RealRooted.BorceaBranden.FiniteSymbolContraction
import RealRooted.BorceaBranden.FiniteSymbolDegree
import RealRooted.BorceaBranden.FiniteSymbolLinearity
import RealRooted.BorceaBranden.FiniteSymbolPreserver
import RealRooted.BorceaBranden.FiniteSymbolProduct
import RealRooted.BorceaBranden.FiniteSymbolReciprocal
import RealRooted.BorceaBranden.FiniteSymbolReconstruction
import RealRooted.BorceaBranden.FiniteSymbolReconstructionCore
import RealRooted.BorceaBranden.UnivariateFiniteSymbol
import RealRooted.BoundarySpecializationRight
import RealRooted.CauchyInterlacing
import RealRooted.CauchyInterlacing.Polynomial
import RealRooted.Challenges.AissenSchoenbergWhitney
import RealRooted.Challenges.BorceaBranden
import RealRooted.Challenges.BrandenSolus
import RealRooted.Challenges.BraunJal
import RealRooted.Challenges.CauchyInterlacing
import RealRooted.Challenges.ChudnovskySeymour
import RealRooted.Challenges.Eulerian
import RealRooted.Challenges.Favard
import RealRooted.Challenges.Hadamard
import RealRooted.Challenges.HermiteBiehlerHurwitz
import RealRooted.Challenges.HermitePoulain
import RealRooted.Challenges.HosterStump
import RealRooted.Challenges.Issue34SingleMatrixCounterexample
import RealRooted.Challenges.Issue34WindowObstruction
import RealRooted.Challenges.Kurtz
import RealRooted.Challenges.MatrixInterlacing
import RealRooted.Challenges.Obreschkoff
import RealRooted.Challenges.OperatorPreservers
import RealRooted.Challenges.VeroneseSections
import RealRooted.Challenges.Wagner
import RealRooted.ChudnovskySeymour
import RealRooted.ClosedSegmentCountEqFromAnalytic
import RealRooted.CoefficientDominance
import RealRooted.CoefficientDominance.LogConcavity
import RealRooted.CoefficientDominance.RootGap
import RealRooted.CoefficientDominance.Sequence
import RealRooted.CoefficientDominance.Symmetric
import RealRooted.CoefficientDominance.Symmetric.Finite
import RealRooted.CoefficientDominance.Symmetric.Polynomial
import RealRooted.CoefficientDominance.Symmetric.Sharp
import RealRooted.CoefficientDominance.Symmetric.Tail
import RealRooted.CoefficientDominance.Symmetric.Upper
import RealRooted.CoefficientShape
import RealRooted.CombinatorialExamples
import RealRooted.CombinatorialExamples.BigDescentsOddBinom
import RealRooted.CombinatorialExamples.ColoredSetPartitions
import RealRooted.CombinatorialExamples.Common
import RealRooted.CombinatorialExamples.Eulerian
import RealRooted.CombinatorialExamples.Motzkin
import RealRooted.CombinatorialExamples.Narayana
import RealRooted.CombinatorialExamples.OneDescentGamma
import RealRooted.CombinatorialExamples.Simsun
import RealRooted.CombinatorialExamples.SingletonFreeSetPartitions
import RealRooted.CombinatorialExamples.StirlingPermutations
import RealRooted.CombinatorialExamples.SturmDerangementsExc
import RealRooted.CombinatorialExamples.Touchard
import RealRooted.CombinatorialExamples.TypeBEulerian
import RealRooted.Combinatorics.OrderedSubsetPairsNarayana
import RealRooted.CommonInterleaver.AffineBoundary
import RealRooted.CommonInterleaver.DescPolynomial
import RealRooted.CommonInterleaver.FamilyUpgrade
import RealRooted.CommonInterleaver.Finite
import RealRooted.CommonInterleaver.IntervalLemmas
import RealRooted.CommonInterleaver.PairBridge
import RealRooted.CommonInterleaver.PairBridge.Compatibility
import RealRooted.CommonInterleaver.PairBridge.Forward
import RealRooted.CommonInterleaver.PairBridge.Reduction
import RealRooted.CommonInterleaver.PairBridge.SuccDegree
import RealRooted.CommonInterleaver.PairwiseUpgrade
import RealRooted.CommonInterleaver.RightPencil
import RealRooted.CommonInterleaver.RootDesc
import RealRooted.CommonInterleaver.RootCountCombinatorics
import RealRooted.CommonInterleaver.RootSlots
import RealRooted.CommonInterleaver.RootSlots.Basic
import RealRooted.CommonInterleaver.Sequence
import RealRooted.CommonInterleaver.SameDegreeRootCount
import RealRooted.CommonInterleaver.Statements
import RealRooted.CommonInterleaver.SuccDegreeEndpoint
import RealRooted.CommonInterleaver.SuccDegreeLowDegree
import RealRooted.CommonInterleaverFamilySum
import RealRooted.CommonInterleaverExamples
import RealRooted.CommonInterleaverSeq
import RealRooted.CommonInterleaverTwo
import RealRooted.Compatibility.Basic
import RealRooted.Compatibility.InterleaverBridge
import RealRooted.Compatibility.Pair
import RealRooted.ComplexCesaro
import RealRooted.ComplexPowers
import RealRooted.ConvexCombination
import RealRooted.CubicDiscriminant
import RealRooted.CubicNewton
import RealRooted.DegreeDropDivXPrec
import RealRooted.DegreeDropReversal
import RealRooted.DegreeIncreasingLocalLowerCount
import RealRooted.Derivative
import RealRooted.Derivative.LinearCombination
import RealRooted.DerivativeRecurrence
import RealRooted.DerivativeRecurrence.Linear
import RealRooted.DerivativeRecurrence.QuadraticDegree
import RealRooted.DerivativeRecurrence.GeneralizedLaguerre
import RealRooted.DerivativeRecurrence.QuadraticInterlacing
import RealRooted.DerivativeRecurrence.QuadraticSeed
import RealRooted.DerivativeRecurrence.QuadraticShift
import RealRooted.DerivativeRecurrence.SecondOrderDegree
import RealRooted.DerivativeRecurrence.SecondDerivativeDegree
import RealRooted.DerivativeShiftRootMatching
import RealRooted.DerivativeShiftSequence
import RealRooted.DeterminantalStability
import RealRooted.DifferentialBlocks
import RealRooted.ElementaryDifferential
import RealRooted.EulerOperator
import RealRooted.EulerOperator.Pencil
import RealRooted.EulerOperator.Polar
import RealRooted.EulerOperator.Polar.ProperPosition
import RealRooted.EulerOperator.ScaledPolar
import RealRooted.EulerianCompletion
import RealRooted.EulerianMixedCompatibility
import RealRooted.EulerianMixedCompatibility.Insertion
import RealRooted.Favard
import RealRooted.Favard.Affine
import RealRooted.Favard.Affine.Basic
import RealRooted.Favard.Affine.Denominator
import RealRooted.Favard.Affine.RowSign
import RealRooted.FiniteFreeMultiplicative
import RealRooted.FiniteFreeRootCount
import RealRooted.FolkloreLemma
import RealRooted.GammaRealRoots
import RealRooted.GammaTransform
import RealRooted.GammaTransform.Basic
import RealRooted.GammaTransform.ProperPosition
import RealRooted.GammaTransform.Preservation
import RealRooted.GammaTransform.RootLists
import RealRooted.GammaTransform.RootMap
import RealRooted.GarloffWagner
import RealRooted.GarloffWagner.Algebra
import RealRooted.GarloffWagner.Iterated
import RealRooted.GarloffWagner.KreinData
import RealRooted.GarloffWagner.KreinExpansion
import RealRooted.GarloffWagner.Theorem12
import RealRooted.GarloffWagner.Hadamard
import RealRooted.GeneralizedEulerian
import RealRooted.GeneralizedLiuWang
import RealRooted.GeneralizedSnakePosets
import RealRooted.GeneralizedSnakePosets.FiniteBoard
import RealRooted.GeneralizedSnakePosets.MatrixInduction
import RealRooted.GeneralizedSnakePosets.Narayana.Claim7
import RealRooted.GeneralizedSnakePosets.Narayana.JacobiTransport
import RealRooted.GeneralizedSnakePosets.Narayana.Modified
import RealRooted.GeneralizedSnakePosets.Narayana.Turan
import RealRooted.GeneralizedSnakePosets.Narayana.TuranCertificates
import RealRooted.GeneralizedSnakePosets.Section3Packages
import RealRooted.GeneralizedSnakePosets.SnakeBoard
import RealRooted.GeneralizedSnakePosets.SnakeCover
import RealRooted.GeneralizedSnakePosets.SnakeReachability
import RealRooted.GeneralizedSnakePosets.SnakeStaircase
import RealRooted.GeneralizedSnakePosets.SnakeWord
import RealRooted.GeneralizedSnakePosets.SquarecaseModel
import RealRooted.GeneralizedSnakePosets.Statements
import RealRooted.GeneralizedSnakePosets.TruncatedStaircase
import RealRooted.GeneralizedSnakePosetsNarayana
import RealRooted.GraceHalfPlane
import RealRooted.GustafssonSolus
import RealRooted.Hadamard
import RealRooted.Hadamard.Basic
import RealRooted.Hadamard.Finite
import RealRooted.Hadamard.Newton
import RealRooted.Hadamard.Cubic
import RealRooted.Hadamard.Grace
import RealRooted.Hadamard.GarloffWagner
import RealRooted.Hadamard.Hurwitz
import RealRooted.Hadamard.Consequences
import RealRooted.HadamardProduct
import RealRooted.HeilmannLieb
import RealRooted.HermiteBiehler
import RealRooted.HermiteBiehler.Basic
import RealRooted.HermiteBiehler.Converse
import RealRooted.HermiteBiehler.Converse.RootGeometry
import RealRooted.HermiteBiehler.Converse.Wronskian
import RealRooted.HermiteBiehler.ConverseLowDegree
import RealRooted.HermiteBiehler.Forward
import RealRooted.HermiteBiehler.Hurwitz
import RealRooted.HermiteBiehler.LogDerivative
import RealRooted.HermiteBiehler.OddEven
import RealRooted.HermitePoulain
import RealRooted.HomogeneousOre
import RealRooted.HomogeneousOreExamples
import RealRooted.HosterStumpInterlacing
import RealRooted.HurwitzMatrix
import RealRooted.InterlacingConeBounds
import RealRooted.InterlacingSequence
import RealRooted.InterlacingSequenceBasic
import RealRooted.Interlacing.Multiplicity
import RealRooted.Interlacing.Residue
import RealRooted.IteratedDerivativeShift
import RealRooted.Jacobi
import RealRooted.JacobiBetaZeroOrthogonality
import RealRooted.JacobiMarkoff
import RealRooted.JacobiOrthogonality
import RealRooted.JacobiParameterInterlacing
import RealRooted.JensenPencilContraction
import RealRooted.JensenPencilPositiveContraction
import RealRooted.Kurtz
import RealRooted.LiebSokal
import RealRooted.LiebSokalOperator
import RealRooted.LiebSokalOperator.Linearity
import RealRooted.LiebSokalPointwise
import RealRooted.Linear
import RealRooted.LinearPowerFamily
import RealRooted.LiuOppositeSigns
import RealRooted.LiuOppositeSigns.BoundedIntervalContinuity
import RealRooted.LiuOppositeSigns.CommonInterleaverConsequences
import RealRooted.LiuOppositeSigns.Corollary22
import RealRooted.LiuOppositeSigns.DeletionBranches
import RealRooted.LiuOppositeSigns.DerivativeShiftRegularization
import RealRooted.LiuOppositeSigns.DerivativeShiftSequenceRegularization
import RealRooted.LiuOppositeSigns.FactorReturnAssembly
import RealRooted.LiuOppositeSigns.FactorReturnLeft
import RealRooted.LiuOppositeSigns.FactorReturnStatements
import RealRooted.LiuOppositeSigns.FactorReturnTwoDegree
import RealRooted.LiuOppositeSigns.ForwardCubicLinear
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.Average
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.LowerSideDouble
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.LowerSideStrict
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.MiddleGap
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RightProtruding
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderAssembly
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderLower
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderMiddle
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderStatement
import RealRooted.LiuOppositeSigns.ForwardCubicQuadratic.RootOrderUpper
import RealRooted.LiuOppositeSigns.ForwardLowDegree
import RealRooted.LiuOppositeSigns.JensenRootCount
import RealRooted.LiuOppositeSigns.NonnegCoeffs
import RealRooted.LiuOppositeSigns.PositiveSplitPair
import RealRooted.LiuOppositeSigns.RootCountClosure
import RealRooted.LiuOppositeSigns.RootCountRelStability
import RealRooted.LiuOppositeSigns.Theorem21Assembly
import RealRooted.LiuOppositeSigns.Theorem21Statements
import RealRooted.LiuOppositeSigns.XSub.CubicCubic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.Basic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.CubicSubQuadratic
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.Endpoints
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.LeftOutlier
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.LeftRepeated
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.MiddleCases
import RealRooted.LiuOppositeSigns.XSub.CubicCubic.RightRepeated
import RealRooted.LiuOppositeSigns.XSub.CubicQuadratic
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.GapCounts
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.LeftSuccessor
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.RightSuccessor
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.RootFilters
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.SameDegree
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.SplitEndpoints
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.TailSigns
import RealRooted.LiuOppositeSigns.XSub.IntervalRootCount.UpperTail
import RealRooted.LiuOppositeSigns.XSub.ProperPosition
import RealRooted.LiuOppositeSigns.XSub.LeftSucc
import RealRooted.LiuOppositeSigns.XSub.LeftSuccDegreeThree
import RealRooted.LiuOppositeSigns.XSub.LeftSuccDegreeTwo
import RealRooted.LiuOppositeSigns.XSub.LinearQuadratic
import RealRooted.LiuOppositeSigns.XSub.QuadraticCubic
import RealRooted.LiuOppositeSigns.XSub.QuadraticQuadratic
import RealRooted.LiuOppositeSigns.XSub.QuarticCubic
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicBoundary
import RealRooted.LiuOppositeSigns.XSub.QuarticCubicCommonRoot
import RealRooted.LiuOppositeSigns.XSub.SameDegree
import RealRooted.LiuOppositeSigns.XSub.SplittingTools
import RealRooted.LiuOppositeSignsTheorem
import RealRooted.LiuWang
import RealRooted.LiuWang.OneAddXPositive
import RealRooted.LiuWang.SequenceCore
import RealRooted.LiuWang.SequenceIntervals
import RealRooted.LiuWang.SequencePositive
import RealRooted.LiuWang.SequenceProducts
import RealRooted.LiuWang.Step
import RealRooted.LiuWangBenchmark
import RealRooted.LiuWangRecursion
import RealRooted.LowerTriangularMatrix
import RealRooted.MaWang
import RealRooted.MaWang.CountBounds
import RealRooted.MaWang.Derivative
import RealRooted.MaWang.DerivativeCore
import RealRooted.MaWang.DerivativeDenominator
import RealRooted.MaWang.DerivativeSequence
import RealRooted.MaWang.DerivativeStep
import RealRooted.MaWang.StrictSigns
import RealRooted.MaWang.StrictSigns.Assembly
import RealRooted.MaWang.StrictSigns.RootSigns
import RealRooted.MaWang.StrictStep
import RealRooted.MaWang.Strong
import RealRooted.MaWang.Weak
import RealRooted.MaWang.Weak.Endpoint
import RealRooted.MaWang.Weak.Regularization
import RealRooted.MaWang.Weak.SameDegree
import RealRooted.MaWang.Weak.Successor
import RealRooted.MagnitudeDominated
import RealRooted.MaoWangMatrixProduct
import RealRooted.Mathlib.Algebra.MvPolynomial.Degrees
import RealRooted.Mathlib.Algebra.MvPolynomial.Equiv
import RealRooted.Mathlib.Algebra.MvPolynomial.EvalOnVars
import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.DegreeBox
import RealRooted.Mathlib.Algebra.MvPolynomial.Stability.Symbol
import RealRooted.Mathlib.Algebra.Order.BigOperators.Alternating
import RealRooted.Mathlib.Algebra.Polynomial.Basic
import RealRooted.Mathlib.Algebra.Polynomial.BasisTransform
import RealRooted.Mathlib.Algebra.Polynomial.Bezoutian
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Algebra
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Basic
import RealRooted.Mathlib.Algebra.Polynomial.CayleyTransform.Roots
import RealRooted.Mathlib.Algebra.Polynomial.Degree.Operations
import RealRooted.Mathlib.Algebra.Polynomial.Degree.SmallDegree
import RealRooted.Mathlib.Algebra.Polynomial.Derivative
import RealRooted.Mathlib.Algebra.Polynomial.Dominance
import RealRooted.Mathlib.Algebra.Polynomial.Eval.Defs
import RealRooted.Mathlib.Algebra.Polynomial.Homogenize
import RealRooted.Mathlib.Algebra.Polynomial.Reverse
import RealRooted.Mathlib.Algebra.Polynomial.Roots
import RealRooted.Mathlib.Algebra.Polynomial.Splits
import RealRooted.Mathlib.Algebra.Polynomial.Splits.Complex
import RealRooted.Mathlib.Algebra.Polynomial.Splits.Derivative
import RealRooted.Mathlib.Analysis.Complex.OpenMapping
import RealRooted.Mathlib.Analysis.Polynomial.MahlerMeasure
import RealRooted.Mathlib.Topology.Algebra.InfiniteSum.Int
import RealRooted.Mathlib.Analysis.SpecialFunctions.ExpIntegral
import RealRooted.Mathlib.Analysis.SpecialFunctions.Integrals.RpowLog
import RealRooted.Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import RealRooted.Mathlib.Combinatorics.Enumerative.OrderedSubsetPairs
import RealRooted.Mathlib.Data.Fin.Basic
import RealRooted.Mathlib.Data.List.Basic
import RealRooted.Mathlib.Data.List.Destutter
import RealRooted.Mathlib.Data.List.Interleave
import RealRooted.Mathlib.Data.List.Interleave.Padding
import RealRooted.Mathlib.Data.List.OfFn
import RealRooted.Mathlib.Data.List.Sort.Endpoint
import RealRooted.Mathlib.Data.List.Zip
import RealRooted.Mathlib.Data.Multiset.Card
import RealRooted.Mathlib.Data.Multiset.Rel
import RealRooted.Mathlib.Data.Nat.Cast.Basic
import RealRooted.Mathlib.Data.Nat.Choose.Cast
import RealRooted.Mathlib.LinearAlgebra.Matrix.Compound
import RealRooted.Mathlib.LinearAlgebra.Matrix.CompoundSpectrum
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.BandedHessenberg
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Basic
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.CauchyBinet
import RealRooted.Mathlib.LinearAlgebra.Matrix.Determinant.Integral
import RealRooted.Mathlib.LinearAlgebra.Matrix.GantmacherKrein
import RealRooted.Mathlib.LinearAlgebra.Matrix.Gaussian
import RealRooted.Mathlib.LinearAlgebra.Matrix.KernelSignVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.Oscillatory
import RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing
import RealRooted.Mathlib.LinearAlgebra.Matrix.OscillatoryInterlacing.Core
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Auxiliary
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.CStarClasses
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.CollatzWielandt
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.DataList
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Dominance
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.ExtremeValueUSC
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Irreducible
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Lemmas
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Nonneg
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Primitive
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.QuiverPath
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Spectrum
import RealRooted.Mathlib.LinearAlgebra.Matrix.PerronFrobenius.Uniqueness
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegular
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularRankDeficient
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularStrictification
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignRegularVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariation
import RealRooted.Mathlib.LinearAlgebra.Matrix.SignVariationTopology
import RealRooted.Mathlib.LinearAlgebra.Matrix.SpectrumClosed
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Charpoly
import RealRooted.Mathlib.LinearAlgebra.Matrix.TotallyNonneg.Mul
import RealRooted.Mathlib.LinearAlgebra.Matrix.Triangularize
import RealRooted.Mathlib.LinearAlgebra.Matrix.VariationDiminishing
import RealRooted.Mathlib.LinearAlgebra.Vandermonde
import RealRooted.Mathlib.RingTheory.MvPolynomial.Symmetric
import RealRooted.Mathlib.RingTheory.Polynomial.Jacobi
import RealRooted.Mathlib.RingTheory.Polynomial.Wronskian
import RealRooted.MatrixInterlacing
import RealRooted.Multiaffine
import RealRooted.MultiaffineReciprocal
import RealRooted.MultiaffineReciprocalRight
import RealRooted.MultiplierSequence
import RealRooted.MultiplierSequence.Bidiagonal
import RealRooted.MultiplierSequence.Bidiagonal.Jensen
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.Contraction
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.CubicResidual
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.CubicResidual.Quadratic
import RealRooted.MultiplierSequence.Bidiagonal.Jensen.LowDegree
import RealRooted.MultiplierSequence.Bidiagonal.SecondDerivative
import RealRooted.MultivariateStability
import RealRooted.NarayanaTransformation
import RealRooted.NarayanaTransformation.Basis
import RealRooted.NarayanaTransformation.Basis.Stirling
import RealRooted.NarayanaTransformation.Coefficients
import RealRooted.NarayanaTransformation.Endpoints
import RealRooted.NarayanaTransformation.Falling
import RealRooted.NarayanaTransformation.Gamma
import RealRooted.NarayanaTransformation.Rectangular
import RealRooted.NarayanaTransformation.Rectangular.LowDegree
import RealRooted.NarayanaTransformation.Rectangular.Narayana
import RealRooted.NarayanaTransformation.Rectangular.Preservation
import RealRooted.NarayanaTransformation.Recurrences
import RealRooted.NarayanaTransformation.Recurrences.Identities
import RealRooted.NarayanaTransformation.Recurrences.Interlacing
import RealRooted.NarayanaTransformation.Rising
import RealRooted.NarayanaTransformation.RootGeometry
import RealRooted.NewtonAux
import RealRooted.OEIS.A046802
import RealRooted.ObreschkoffContinuity
import RealRooted.ObreschkoffConverse
import RealRooted.ObreschkoffConverse.Converse
import RealRooted.ObreschkoffConverse.DegreeGap
import RealRooted.ObreschkoffConverse.Derivative
import RealRooted.ObreschkoffConverse.Forward
import RealRooted.ObreschkoffConverse.Regularization
import RealRooted.OscillatoryInterlacing
import RealRooted.OperatorPreservesInterlacing
import RealRooted.OrderedRoots
import RealRooted.ParkingFunctions.ToricContribution.CommonInterlacer
import RealRooted.ParkingFunctions.ToricContribution.ContributionReversal
import RealRooted.ParkingFunctions.ToricContribution.Definitions
import RealRooted.ParkingFunctions.ToricContribution.DiagonalCollapse
import RealRooted.ParkingFunctions.ToricContribution.ExceptionalOffset
import RealRooted.ParkingFunctions.ToricContribution.FiniteOffsets
import RealRooted.ParkingFunctions.ToricContribution.IntervalInsertion
import RealRooted.ParkingFunctions.ToricContribution.TriangleInvariant
import RealRooted.ParkingFunctions.ToricContribution.TriangleAlgebra
import RealRooted.PFPolynomial
import RealRooted.PartialSumStep
import RealRooted.PartialSymmetrization
import RealRooted.Polarization
import RealRooted.PolyaFrequencyConvolution
import RealRooted.PosCombo
import RealRooted.PositiveParameterLocalLowerCount
import RealRooted.ProductFamily
import RealRooted.ProductOrientation
import RealRooted.ProductSequence
import RealRooted.QuadraticCubicPencil
import RealRooted.QuadraticRoot
import RealRooted.RankTwoMatching
import RealRooted.RankTwoMatching.Basic
import RealRooted.RankTwoMatching.DisjointEquiv
import RealRooted.RankTwoMatching.Endpoint
import RealRooted.RankTwoMatching.Enumeration
import RealRooted.RankTwoMatching.Orientation
import RealRooted.RankTwoMatching.Transform
import RealRooted.RankTwoMatchingModel
import RealRooted.RectangularConvolution
import RealRooted.RectangularConvolutionIdentity
import RealRooted.RectangularPolarization
import RealRooted.RectangularPolarizationComplement
import RealRooted.RecurrenceDiscriminant
import RealRooted.ReflectedRootCountLocalConstancy
import RealRooted.ReciprocalShift.Interlacing
import RealRooted.ReciprocalShift.Interlacing.Inversion
import RealRooted.ReciprocalShift.ProperPosition
import RealRooted.ReciprocalShift.Roots
import RealRooted.RootAmplitude
import RealRooted.RootAmplitude.Convex
import RealRooted.RootAmplitude.Density
import RealRooted.RootAmplitude.Extension
import RealRooted.RootAmplitude.Extreme
import RealRooted.RootAmplitude.Finite
import RealRooted.RootAmplitude.Minimum
import RealRooted.RootAmplitude.Polynomial
import RealRooted.RootAmplitude.SumSquares
import RealRooted.RootBounds
import RealRooted.RootContinuity
import RealRooted.RootCountFinite
import RealRooted.RootCountJump
import RealRooted.RootCountLocalConstancy
import RealRooted.RootCounting
import RealRooted.RootCounting.Finite
import RealRooted.RootCounting.SignChanges
import RealRooted.RootCounting.Threshold
import RealRooted.RootCounting.Threshold.Anchor
import RealRooted.RootCounting.Threshold.Basic
import RealRooted.RootCounting.Threshold.Derivative
import RealRooted.RootCounting.Threshold.LogConcavity
import RealRooted.RootCounting.Threshold.Signs
import RealRooted.RootCounting.Threshold.Sorted
import RealRooted.RootMatchingSort
import RealRooted.RootMultiplicityMatching
import RealRooted.RootOrderBridge
import RealRooted.RootSumBounds
import RealRooted.RootVieta
import RealRooted.RowThreshold
import RealRooted.RowThresholdOne
import RealRooted.SameDegreeCountFromAnalytic
import RealRooted.SameDegreeCubicRootCount
import RealRooted.SameDegreeCubicSecondRootFromAnalytic
import RealRooted.SameDegreeDerivative
import RealRooted.SameDegreeMultiplicityLowerCount
import RealRooted.SameDegreeQuadraticObstruction
import RealRooted.SameDegreeQuadraticRootCount
import RealRooted.ScalarNormalization
import RealRooted.SequenceClosure
import RealRooted.ShiftLemma
import RealRooted.SignEvaluation
import RealRooted.SmallPositiveParameterCount
import RealRooted.SimpleRoots
import RealRooted.SortedRoots
import RealRooted.SortedRoots.Exhibited
import RealRooted.StaircaseSum
import RealRooted.SuccDegreeLeftEndpoint
import RealRooted.SuccDegreeRootCrossing
import RealRooted.SymmetricDecomposition
import RealRooted.SymmetricDecomposition.Decomposition
import RealRooted.SymmetricDecomposition.Definitions
import RealRooted.SymmetricDecomposition.FPolynomial
import RealRooted.SymmetricDecomposition.FPolynomialInterlacing
import RealRooted.SymmetricDecomposition.Theorem26
import RealRooted.Tactic
import RealRooted.Tactic.AffineDerivative
import RealRooted.Tactic.AissenSchoenbergWhitney
import RealRooted.Tactic.AllCombo
import RealRooted.Tactic.Attr
import RealRooted.Tactic.Bezoutian
import RealRooted.Tactic.CoefficientShape
import RealRooted.Tactic.CommonInterleaver
import RealRooted.Tactic.CubicDiscriminant
import RealRooted.Tactic.Derivative
import RealRooted.Tactic.EndpointDerivative
import RealRooted.Tactic.EulerOperator
import RealRooted.Tactic.Examples
import RealRooted.Tactic.Examples.AffineDerivative
import RealRooted.Tactic.Examples.AissenSchoenbergWhitney
import RealRooted.Tactic.Examples.AllCombo
import RealRooted.Tactic.Examples.Attr
import RealRooted.Tactic.Examples.Bezoutian
import RealRooted.Tactic.Examples.CoefficientShape
import RealRooted.Tactic.Examples.Combinatorial
import RealRooted.Tactic.Examples.CommonInterleaver
import RealRooted.Tactic.Examples.CubicDiscriminant
import RealRooted.Tactic.Examples.Derivative
import RealRooted.Tactic.Examples.EndpointDerivative
import RealRooted.Tactic.Examples.EulerOperator
import RealRooted.Tactic.Examples.Favard
import RealRooted.Tactic.Examples.Finish
import RealRooted.Tactic.Examples.FiniteSymbol
import RealRooted.Tactic.Examples.FiniteSymbolPF
import RealRooted.Tactic.Examples.GammaRealRoots
import RealRooted.Tactic.Examples.Hadamard
import RealRooted.Tactic.Examples.HermiteBiehler
import RealRooted.Tactic.Examples.HermitePoulain
import RealRooted.Tactic.Examples.HomogenizeStable
import RealRooted.Tactic.Examples.I2DerivativeLag
import RealRooted.Tactic.Examples.InterlacingSequence
import RealRooted.Tactic.Examples.IteratedDerivativeShift
import RealRooted.Tactic.Examples.IteratedDerivativeShiftProduct
import RealRooted.Tactic.Examples.J1Chebyshev
import RealRooted.Tactic.Examples.J1Gap3Reciprocal
import RealRooted.Tactic.Examples.Kurtz
import RealRooted.Tactic.Examples.Linear
import RealRooted.Tactic.Examples.LinearPowerFamily
import RealRooted.Tactic.Examples.LiuWang
import RealRooted.Tactic.Examples.LiuWangRecursion
import RealRooted.Tactic.Examples.Lookup
import RealRooted.Tactic.Examples.MaWang
import RealRooted.Tactic.Examples.MagnitudeDominated
import RealRooted.Tactic.Examples.Matrix
import RealRooted.Tactic.Examples.MultiplierSequence
import RealRooted.Tactic.Examples.Narayana
import RealRooted.Tactic.Examples.OEIS
import RealRooted.Tactic.Examples.OEISPositiveTLag
import RealRooted.Tactic.Examples.OEISTestbed
import RealRooted.Tactic.Examples.OperatorPreservesInterlacing
import RealRooted.Tactic.Examples.PFBidiagonal
import RealRooted.Tactic.Examples.PFPolynomial
import RealRooted.Tactic.Examples.PosCombo
import RealRooted.Tactic.Examples.PreservingOperatorSequence
import RealRooted.Tactic.Examples.Product
import RealRooted.Tactic.Examples.ReciprocalShift
import RealRooted.Tactic.Examples.RecurrenceIdentification
import RealRooted.Tactic.Examples.RootBounds
import RealRooted.Tactic.Examples.RootCount
import RealRooted.Tactic.Examples.ScalarDen
import RealRooted.Tactic.Examples.SecondDerivative
import RealRooted.Tactic.Examples.SequenceSurvey
import RealRooted.Tactic.Examples.SideGoals
import RealRooted.Tactic.Examples.Sign
import RealRooted.Tactic.Examples.SignAssembly
import RealRooted.Tactic.Examples.StaircaseSum
import RealRooted.Tactic.Examples.SymmetricDecomposition
import RealRooted.Tactic.Examples.VeroneseSection
import RealRooted.Tactic.Examples.Wagner
import RealRooted.Tactic.Examples.WagnerX
import RealRooted.Tactic.Examples.WeightedSum
import RealRooted.Tactic.Favard
import RealRooted.Tactic.Favard.Basic
import RealRooted.Tactic.Favard.Denominator
import RealRooted.Tactic.Favard.DenominatorSyntax
import RealRooted.Tactic.Favard.Direct
import RealRooted.Tactic.Favard.DirectSyntax
import RealRooted.Tactic.Favard.RowSign
import RealRooted.Tactic.Favard.RowSignSyntax
import RealRooted.Tactic.Finish
import RealRooted.Tactic.FiniteSymbol
import RealRooted.Tactic.FiniteSymbolPF
import RealRooted.Tactic.GammaRealRoots
import RealRooted.Tactic.Hadamard
import RealRooted.Tactic.HermiteBiehler
import RealRooted.Tactic.HermitePoulain
import RealRooted.Tactic.HomogenizeStable
import RealRooted.Tactic.I2DerivativeLag
import RealRooted.Tactic.InterlacingSequence
import RealRooted.Tactic.IteratedDerivativeShift
import RealRooted.Tactic.IteratedDerivativeShiftProduct
import RealRooted.Tactic.J1Chebyshev
import RealRooted.Tactic.J1Gap3Reciprocal
import RealRooted.Tactic.Kurtz
import RealRooted.Tactic.Linear
import RealRooted.Tactic.LinearPowerFamily
import RealRooted.Tactic.LiuWang
import RealRooted.Tactic.LiuWang.SequenceIntervals
import RealRooted.Tactic.LiuWang.SequenceNonpositive
import RealRooted.Tactic.LiuWang.SequencePositive
import RealRooted.Tactic.LiuWang.SequenceProducts
import RealRooted.Tactic.LiuWang.SequenceQuadratic
import RealRooted.Tactic.LiuWang.Step
import RealRooted.Tactic.LiuWangRecursion
import RealRooted.Tactic.Lookup
import RealRooted.Tactic.MaWang
import RealRooted.Tactic.MaWang.Basic
import RealRooted.Tactic.MaWang.Denominator
import RealRooted.Tactic.MaWang.DenominatorSyntax
import RealRooted.Tactic.MaWang.Factors
import RealRooted.Tactic.MaWang.FactorSyntax
import RealRooted.Tactic.MaWang.Sequences
import RealRooted.Tactic.MaWang.SequenceSyntax
import RealRooted.Tactic.MaWang.Steps
import RealRooted.Tactic.MaWang.StepSyntax
import RealRooted.Tactic.MagnitudeDominated
import RealRooted.Tactic.Matrix
import RealRooted.Tactic.MultiplierSequence
import RealRooted.Tactic.Named
import RealRooted.Tactic.Narayana
import RealRooted.Tactic.OEIS
import RealRooted.Tactic.OEIS.Basic
import RealRooted.Tactic.OEIS.DerivativeLag
import RealRooted.Tactic.OEIS.NegativeLag
import RealRooted.Tactic.OEIS.PositiveLag
import RealRooted.Tactic.OEIS.ProductExit
import RealRooted.Tactic.OEIS.ProductFactor
import RealRooted.Tactic.OEIS.ProductLift
import RealRooted.Tactic.OEIS.ProductParity
import RealRooted.Tactic.OperatorPreservesInterlacing
import RealRooted.Tactic.PFBidiagonal
import RealRooted.Tactic.PFPolynomial
import RealRooted.Tactic.PosCombo
import RealRooted.Tactic.PreservingOperatorSequence
import RealRooted.Tactic.Product
import RealRooted.Tactic.ReciprocalShift
import RealRooted.Tactic.RecurrenceEval
import RealRooted.Tactic.RecurrenceIdentification
import RealRooted.Tactic.RootBounds
import RealRooted.Tactic.RootCount
import RealRooted.Tactic.ScalarDen
import RealRooted.Tactic.SecondDerivative
import RealRooted.Tactic.SideGoals
import RealRooted.Tactic.Sign
import RealRooted.Tactic.SignAssembly
import RealRooted.Tactic.StaircaseSum
import RealRooted.Tactic.SymmetricDecomposition
import RealRooted.Tactic.Targets
import RealRooted.Tactic.VeroneseSection
import RealRooted.Tactic.Wagner
import RealRooted.Tactic.WagnerX
import RealRooted.Tactic.WagnerX.Core
import RealRooted.Tactic.WagnerX.Frontend
import RealRooted.Tactic.WagnerX.Obstructions
import RealRooted.Tactic.WagnerX.PositiveLag
import RealRooted.Tactic.WagnerX.Syntax
import RealRooted.Tactic.WagnerX.TranslatedLag
import RealRooted.Tactic.WeightedSum
import RealRooted.ThresholdMatrix
import RealRooted.Touchard
import RealRooted.TridiagonalDet
import RealRooted.UpperDerivativeInterlace
import RealRooted.VeroneseMatrix
import RealRooted.VeroneseSection
import RealRooted.VeroneseSectionPair
import RealRooted.VeroneseSectionPair.HermiteBiehler
import RealRooted.Wagner
import RealRooted.Wagner.NonpositiveRoots
import RealRooted.WagnerLeftSum
import RealRooted.WagnerRightSum
import RealRooted.WagnerX
import RealRooted.WagnerX.AffineFactors
import RealRooted.WagnerX.ListInterlacing
import RealRooted.WagnerX.NonnegativeRoots
import RealRooted.WagnerX.ProperPosition
import RealRooted.WeightedSum
import RealRooted.Wronskian
import RealRooted.Wronskian.Algebra
import RealRooted.Wronskian.Converse
import RealRooted.Wronskian.Forward
import RealRooted.Wronskian.Successor
import RealRooted.Wronskian.Successor.Gap
import RealRooted.Wronskian.Successor.Interlacing
import RealRooted.Wronskian.Successor.Signs
import RealRooted.Wronskian.Successor.Splits