Theorems
Hadamard products and Schur–Szegő composition
Schur–Szegő composition and coefficientwise products preserve several real-rootedness and interlacing classes. This page also covers the finite Pólya–Schur theorem and Maló’s theorem on totally nonnegative Toeplitz matrices.
The results of Garloff and Wagner for PF polynomials (real-rooted with nonnegative coefficients):
- PF closure: the Hadamard product $\sum_k a_k b_k x^k$ of two PF polynomials is PF.
- Interlacing: if $f \ll g$ and $p \ll q$, then $f \ast p \ll g \ast q$, where $\ast$ is the Hadamard product.
- Schur product (Theorem 12): the factorial Schur product, with coefficients $k!\, a_k b_k$, preserves interlacing in its first argument.
References
E. Maló, “Note sur les équations algébriques dont toutes les racines sont réelles,” Journal de Mathématiques Spéciales 4 (1895), 7–10; G. Pólya and I. Schur, “Über zwei Arten von Faktorenfolgen in der Theorie der algebraischen Gleichungen,” Journal für die reine und angewandte Mathematik 144 (1914), 89–113; D. G. Wagner, “Total positivity of Hadamard products,” Journal of Mathematical Analysis and Applications 163 (1992), 459–483; J. Garloff and D. G. Wagner, “Hadamard products of stable polynomials are stable,” Journal of Mathematical Analysis and Applications 202 (1996), 797–809. See the Hadamard-product overview and Schur–Szegő composition on symmetricfunctions.com.
≔ Definitions
Schur–Szegő composition
def schurSzegoComp (n : Nat) (f g : ℝ[X]) : ℝ[X] :=
Finset.sum (Finset.range (n + 1))
(fun k => monomial k (f.coeff k * g.coeff k / (Nat.choose n k : ℝ)))
Hadamard product
def hadamardProduct (p q : ℝ[X]) : ℝ[X] :=
p.sum fun n a => monomial n (a * q.coeff n)
PF polynomial
def IsPFPolynomial (p : ℝ[X]) : Prop :=
HasNonnegCoeffs p ∧ (p = 0 ∨ p.Splits) ∧ ∀ r ∈ p.roots, r ≤ 0
Toeplitz matrix of a sequence
def toeplitz {R : Type*} [Zero R] (a : ℕ → R) : Matrix ℕ ℕ R :=
.of fun i j ↦ if j ≤ i then a (i - j) else 0
Factorial Schur product
def gwSchurProduct (p q : ℝ[X]) : ℝ[X] :=
diagonalOperator (fun k => (Nat.factorial k : ℝ) * q.coeff k) p
⊢ Theorems
Schur–Szegő composition preserves real-rootedness
theorem finiteSchurSzegoComposition :
∀ {n : ℕ} {f p : ℝ[X]},
IsPFPolynomial f →
f.natDegree ≤ n →
p.natDegree ≤ n →
p.Splits →
schurSzegoComp n f p = 0 ∨ (schurSzegoComp n f p).Splits
Finite Pólya–Schur theorem
theorem finitePolyaSchur_nonneg :
∀ {n : ℕ} {gamma : ℕ → ℝ},
(∀ k, 0 ≤ gamma k) →
(IsFiniteMultiplierSequence n gamma ↔
IsPFPolynomial (jensenPolynomial n gamma))
Hadamard products preserve interlacing
theorem garloffWagnerHadamardNonnegInterl :
∀ {f g p q : ℝ[X]},
HasNonnegCoeffs f → HasNonnegCoeffs g →
HasNonnegCoeffs p → HasNonnegCoeffs q →
StrictInterl f g → StrictInterl p q →
Interl (hadamardProduct f p) (hadamardProduct g q)
Maló: Hadamard products of totally nonnegative Toeplitz matrices
theorem maloToeplitzHadamard {p q : ℝ[X]}
(hp : (toeplitz p.coeff).IsTotallyNonneg)
(hq : (toeplitz q.coeff).IsTotallyNonneg) :
(Matrix.of fun i j =>
toeplitz p.coeff i j * toeplitz q.coeff i j).IsTotallyNonneg
Products of polynomial value sequences are PF
theorem polynomialValueProductPolyaFrequency
{f g : ℝ[X]} (hf : IsPolyaFreqSeq (polynomialValueSeq f))
(hg : IsPolyaFreqSeq (polynomialValueSeq g)) :
IsPolyaFreqSeq (polynomialValueSeq (f * g))
Garloff–Wagner: Hadamard products of PF polynomials are PF
theorem gwHadamardProductPF {p q : ℝ[X]}
(hp : IsPFPolynomial p) (hq : IsPFPolynomial q) :
IsPFPolynomial (hadamardProduct p q)
Garloff–Wagner: Hadamard products preserve interlacing
theorem gwHadamardProductInterl_of_strictInterl {f g p q : ℝ[X]}
(hf : IsPFPolynomial f) (hg : IsPFPolynomial g)
(hp : IsPFPolynomial p) (hq : IsPFPolynomial q)
(hfg : StrictInterl f g) (hpq : StrictInterl p q) :
Interl (hadamardProduct f p) (hadamardProduct g q)
Garloff–Wagner, Theorem 12: the Schur product preserves interlacing
theorem gwSchurProductInterl :
∀ {f g p : ℝ[X]},
IsPFPolynomial f →
IsPFPolynomial g →
IsPFPolynomial p →
Interl f g →
Interl (gwSchurProduct f p) (gwSchurProduct g p)
Lean source RealRooted/Challenges/Hadamard.lean at revision 5827550b.