Multiplier sequences

A real sequence $\gamma = (\gamma_0, \gamma_1, \dotsc)$ is a multiplier sequence if the diagonal operator

a_0 + a_1 x + \dotsb + a_n x^n \;\mapsto\; \gamma_0 a_0 + \gamma_1 a_1 x + \dotsb + \gamma_n a_n x^n

sends every real-rooted polynomial to a real-rooted polynomial (or zero). It is a PF multiplier sequence if it preserves real-rootedness with nonnegative coefficients. The finite version restricts to inputs of degree at most $n$.

The following hold:

Jensen polynomials (Pólya–Schur): a nonnegative sequence is a multiplier sequence if and only if every Jensen polynomial $g_n(x) = \sum_k \binom{n}{k} \gamma_k x^k$ has only real nonpositive zeros.
Laguerre–Pólya classification (Pólya–Schur): under a growth condition, $\gamma$ is a PF multiplier sequence if and only if its exponential generating function $\sum_k \gamma_k z^k/k!$ is a locally uniform limit of PF polynomials, that is, lies in the Laguerre–Pólya class of type I. Without the sign condition, $\gamma$ is a multiplier sequence if and only if one of $\pm f(\pm z)$ is of type I, where $f$ is the generating function; equivalently, one of $\pm\gamma_k$ and $\pm(-1)^k \gamma_k$ is a PF multiplier sequence.
Log-concavity: PF multiplier sequences are log-concave.
Laguerre's theorem: if a polynomial $\varphi$ has only real nonpositive zeros, then $\varphi(0), \varphi(1), \varphi(2), \dotsc$ is a multiplier sequence. It is a PF multiplier sequence when the leading coefficient is nonnegative. The basic case $k + r$, for real $r \geq 0$, has Jensen polynomials $(1+x)^{n-1}\bigl((n+r)x+r\bigr)$. More generally, if $f$ is a locally uniform limit of PF polynomials (type I in the Laguerre–Pólya class), then $f(0), f(1), f(2), \dotsc$ is a PF multiplier sequence.
Examples: for real $\alpha > 0$, the reciprocal rising factorials $1/(\alpha)_k$ form a PF multiplier sequence, and so in particular do $1/k!$. After clearing denominators, their Jensen polynomials are generalized Laguerre polynomials.

References

G. Pólya and J. Schur, “Über zwei Arten von Faktorenfolgen in der Theorie der algebraischen Gleichungen,” J. Reine Angew. Math. 144 (1914), 89–113. The finite Pólya–Schur theorem through the Schur–Szegő composition is on the Hadamard products page.

Definitions

Diagonal operator of a sequence

RealRooted.diagonalOperatorsource

def diagonalOperator (gamma : ℕ → ℝ) (p : ℝ[X]) : ℝ[X] :=
  p.sum fun n a => monomial n (gamma n * a)

Jensen polynomials

RealRooted.jensenPolynomialsource

def jensenPolynomial (n : ℕ) (gamma : ℕ → ℝ) : ℝ[X] :=
  ∑ k ∈ Finset.range (n + 1),
    monomial k ((Nat.choose n k : ℝ) * gamma k)

Finite multiplier sequence

RealRooted.IsFiniteMultiplierSequencesource

def IsFiniteMultiplierSequence (n : ℕ) (gamma : ℕ → ℝ) : Prop :=
  ∀ {p : ℝ[X]},
    p.natDegree ≤ n →
    p.Splits →
    diagonalOperator gamma p = 0 ∨ (diagonalOperator gamma p).Splits

Multiplier sequence

RealRooted.IsMultiplierSequencesource

def IsMultiplierSequence (gamma : ℕ → ℝ) : Prop :=
  ∀ n : ℕ, IsFiniteMultiplierSequence n gamma

PF multiplier sequence

RealRooted.IsPFMultiplierSequencesource

def IsPFMultiplierSequence (gamma : ℕ → ℝ) : Prop :=
  ∀ n : ℕ, IsFinitePFMultiplierSequence n gamma

Laguerre–Pólya class of type I

RealRooted.IsLaguerrePolyaTypeIsource

def IsLaguerrePolyaTypeI (f : ℂ → ℂ) : Prop :=
  ∃ p : ℕ → ℝ[X],
    (∀ n, IsPFPolynomial (p n)) ∧
      TendstoLocallyUniformly
        (fun n (z : ℂ) => (p n).map Complex.ofRealHom |>.eval z) f atTop

Theorems

Pólya–Schur: multiplier sequences via Jensen polynomialsMain result

RealRooted.isMultiplierSequence_iff_jensenPolynomial_isPFsource

theorem isMultiplierSequence_iff_jensenPolynomial_isPF
    {gamma : ℕ → ℝ} (hgamma : ∀ k, 0 ≤ gamma k) :
    IsMultiplierSequence gamma ↔
      ∀ n : ℕ, IsPFPolynomial (jensenPolynomial n gamma)

Pólya–Schur: PF multiplier sequences are the Laguerre–Pólya type I classMain result

RealRooted.isPFMultiplierSequence_iff_isLaguerrePolyaTypeI_complexExpGeneratingFunctionsource

theorem isPFMultiplierSequence_iff_isLaguerrePolyaTypeI_complexExpGeneratingFunction
    {gamma : ℕ → ℝ}
    (hpositive : ∃ R : NNReal, 0 < R ∧
      Summable (fun k => ‖gamma k‖ * (R : ℝ) ^ k / k.factorial)) :
    IsPFMultiplierSequence gamma ↔
      IsLaguerrePolyaTypeI (complexExpGeneratingFunction gamma)

Pólya–Schur: classification of all multiplier sequencesMain result

RealRooted.isMultiplierSequence_iff_isLaguerrePolyaTypeISigned_complexExpGeneratingFunctionsource

theorem isMultiplierSequence_iff_isLaguerrePolyaTypeISigned_complexExpGeneratingFunction
    {gamma : ℕ → ℝ}
    (hpositive : ∃ R : NNReal, 0 < R ∧
      Summable (fun k => ‖gamma k‖ * (R : ℝ) ^ k / k.factorial)) :
    IsMultiplierSequence gamma ↔
      IsLaguerrePolyaTypeISigned (complexExpGeneratingFunction gamma)

Every multiplier sequence is a PF one up to signs

RealRooted.IsMultiplierSequence.exists_pf_sign_normalizationsource

theorem IsMultiplierSequence.exists_pf_sign_normalization
    {gamma : ℕ → ℝ} (hgamma : IsMultiplierSequence gamma) :
    (IsPFMultiplierSequence gamma ∨
        IsPFMultiplierSequence (fun k => -gamma k)) ∨
      (IsPFMultiplierSequence (fun k => (-1 : ℝ) ^ k * gamma k) ∨
        IsPFMultiplierSequence (fun k => -((-1 : ℝ) ^ k * gamma k)))

PF multiplier sequences are log-concave

RealRooted.IsPFMultiplierSequence.logConcavesource

theorem IsPFMultiplierSequence.logConcave {gamma : ℕ → ℝ}
    (hgamma : IsPFMultiplierSequence gamma) (k : ℕ) :
    gamma k * gamma (k + 2) ≤ gamma (k + 1) ^ 2

Reciprocal rising factorials 1/(α)ₖ form a PF multiplier sequence

RealRooted.isPFMultiplierSequence_inv_ascPochhammersource

theorem isPFMultiplierSequence_inv_ascPochhammer {α : ℝ} (hα : 0 < α) :
    IsPFMultiplierSequence (fun k => ((ascPochhammer ℝ k).eval α)⁻¹)

1/k! is a PF multiplier sequence

RealRooted.isPFMultiplierSequence_inv_factorialsource

theorem isPFMultiplierSequence_inv_factorial :
    IsPFMultiplierSequence (fun k => ((k.factorial : ℝ))⁻¹)

Laguerre's theorem: φ(0), φ(1), … is a multiplier sequenceMain result

RealRooted.isMultiplierSequence_eval_of_roots_nonpossource

theorem isMultiplierSequence_eval_of_roots_nonpos {φ : ℝ[X]} (hφ : φ.Splits)
    (hroots : ∀ r ∈ φ.roots, r ≤ 0) :
    IsMultiplierSequence (fun k => φ.eval (k : ℝ))

k + r is a PF multiplier sequence for r ≥ 0

RealRooted.isPFMultiplierSequence_natCast_addsource

theorem isPFMultiplierSequence_natCast_add {r : ℝ} (hr : 0 ≤ r) :
    IsPFMultiplierSequence (fun k => (k : ℝ) + r)

Type I functions sampled at 0, 1, 2, … are PF multiplier sequences

RealRooted.IsLaguerrePolyaTypeI.isPFMultiplierSequence_eval_natCastsource

theorem IsLaguerrePolyaTypeI.isPFMultiplierSequence_eval_natCast {f : ℂ → ℂ}
    (hf : IsLaguerrePolyaTypeI f) :
    IsPFMultiplierSequence (fun k => (f k).re)

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

Multiplier sequences

References

≔ Definitions

⊢ Theorems

Definitions

Theorems