Theorems

Hermite–Poulain theorem

For a polynomial $f(x) = \sum_k a_k x^k$, write $f(D) = \sum_k a_k D^k$, where $D = d/dx$. If $f$ and $p$ are real-rooted, then $f(D)\,p$ is zero or real-rooted.

References

The theorem goes back to Hermite and Poulain; see the Hermite–Poulain theorem on symmetricfunctions.com for further references.

Definitions

  • The operator f(D)

    RealRooted.HermitePoulain.applyAsDifferentialOperatorsource
    def applyAsDifferentialOperator (f g : ℝ[X]) : ℝ[X] :=
  (Finset.range (f.natDegree + 1)).sum fun k =>
    C (f.coeff k) * ((derivative^[k]) g)

Theorems

  • Hermite–Poulain theorem

    RealRooted.HermitePoulain.differential_operator_preserves_real_rootedsource
    theorem differential_operator_preserves_real_rooted {f g : ℝ[X]}
    (hf : f ≠ 0 ∧ f.Splits)
    (hg : g ≠ 0 ∧ g.Splits) :
    applyAsDifferentialOperator f g = 0 ∨
      (applyAsDifferentialOperator f g).Splits

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