The Hermite–Biehler theorem characterizes half-plane stability through interlacing of the even and odd parts. The Hurwitz criterion characterizes weak Hurwitz stability by total nonnegativity of the classical Hurwitz matrix.
O. Holtz, “Hermite–Biehler, Routh–Hurwitz, and total positivity,” Linear Algebra and its Applications 372 (2003), 105–110. See also the Hermite–Biehler theorem and Hurwitz criterion on symmetricfunctions.com.
Hermite–Biehler: interlacing gives stability
theorem hermiteBiehler_forward :
∀ {f g : ℝ[X]},
HasPosLeadingCoeff f →
HasPosLeadingCoeff g →
StrictInterl g f →
IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g)Hermite–Biehler: stability gives interlacing
theorem hermiteBiehler_converse :
∀ ⦃f g : ℝ[X]⦄,
HasPosLeadingCoeff f →
HasPosLeadingCoeff g →
IsUpperHalfPlaneStable (hermiteBiehlerPolynomial f g) →
StrictInterl g f ∨ StrictInterl f gHurwitz criterion via total nonnegativity
theorem classicalHurwitzCriterion {p : ℝ[X]} (hp : p ≠ 0) :
RealRooted.IsHurwitzStable p ↔
(Matrix.hurwitz p.coeff).IsTotallyNonnegLean source RealRooted/Challenges/HermiteBiehlerHurwitz.lean at revision 5827550b.