Theorems

Aissen–Schoenberg–Whitney

A finite sequence of nonnegative reals is a Pólya frequency sequence if and only if its generating polynomial has only real, nonpositive zeros. Both directions are proved.

References

M. Aissen, I. J. Schoenberg, and A. M. Whitney, “On the generating functions of totally positive sequences. I,” Journal d’Analyse Mathématique 2 (1952), 93–103. See the Pólya-frequency overview on symmetricfunctions.com.

Definitions

  • Pólya frequency sequence

    RealRooted.IsPolyaFreqSeqsource
    def IsPolyaFreqSeq (a : ℕ → ℝ) : Prop :=
  (toeplitz a).IsTotallyNonneg

Theorems

  • PF coefficients give real nonpositive zeros

    RealRooted.Challenges.AissenSchoenbergWhitney.forwardTheoremsource
    theorem forwardTheorem :
    ∀ {p : ℝ[X]}, IsPolyaFreqSeq p.coeff →
      p.Splits ∧ ∀ r ∈ p.roots, r ≤ 0

  • Real nonpositive zeros give PF coefficients

    RealRooted.Challenges.AissenSchoenbergWhitney.reverseTheoremsource
    theorem reverseTheorem :
    ∀ {p : ℝ[X]},
      HasNonnegCoeffs p →
      (p.Splits ∧ ∀ r ∈ p.roots, r ≤ 0) →
      IsPolyaFreqSeq p.coeff

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