Theorems

Kurtz’s coefficient criterion

If a polynomial has positive coefficients and $a_k^2 > 4a_{k-1}a_{k+1}$ at every interior index, then all its roots are real and distinct.

References

D. C. Kurtz, “A sufficient condition for all the roots of a polynomial to be real,” American Mathematical Monthly 99 (1992), 259–263. See also the contextual account on symmetricfunctions.com.

Definitions

  • Positive coefficients

    RealRooted.Kurtz.PositiveCoeffsUpToDegreesource
    def PositiveCoeffsUpToDegree (p : ℝ[X]) : Prop :=
  ∀ i ≤ p.natDegree, 0 < p.coeff i

  • Kurtz inequalities a_k² > 4 a_{k-1} a_{k+1}

    RealRooted.Kurtz.KurtzStrictInequalitiessource
    def KurtzStrictInequalities (p : ℝ[X]) : Prop :=
  ∀ i : ℕ, 0 < i → i < p.natDegree →
    4 * p.coeff (i - 1) * p.coeff (i + 1) < (p.coeff i) ^ 2

Theorems

  • Kurtz's criterion

    RealRooted.Kurtz.coefficient_criterionsource
    theorem coefficient_criterion {p : ℝ[X]}
    (hdeg : 2 ≤ p.natDegree)
    (hpos : PositiveCoeffsUpToDegree p)
    (hineq : KurtzStrictInequalities p) :
    p.Splits

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