Theorems

Totally nonnegative matrices and chain polynomials

A lower-triangular matrix $A$ defines chain polynomials by $P_0 = 1$ and

$$P_{n+1}(x) = x \sum_{k \leq n} A(n+1,k)\, P_k(x).$$

When $A$ counts weighted chains in a poset, $P_n$ enumerates the chains by length.

Theorem (Brändén–Saud Leite, Theorem 3.7). If $A$ is lower unitriangular and totally nonnegative, then every $P_n$ has nonnegative coefficients and only real zeros in $[-1, 0]$, and $P_n$ interlaces $P_{n+1}$.

The matrices covered are exactly the resolvable ones: a lower-unitriangular matrix admits a resolution by nonnegative weights and monic polynomials if and only if it is totally nonnegative. The same conclusion holds for totally nonnegative matrices with a positive constant diagonal.

Applied to power-series kernels built from Pólya frequency sequences, the theorem gives PF polynomials whose consecutive rows interlace, for two row families:

In particular, the rows of $1/\bigl(1 - xz(1+z)^d\bigr)$ and of $1/\bigl(1 - xz/(1-z)^e\bigr)$ are PF and interlace. These include OEIS A116088 ($d = 2$), A116089 ($d = 3$) and A206294 ($e = 3$).

The resolution theorem has a network form. Every lower-unitriangular totally nonnegative matrix is the path matrix of a triangular planar network whose nonnegative weights come from Whitney elimination. The same machinery gives PF rows for tiling polynomials built from weighted lower shifts.

Proof idea

Whitney elimination factors a totally nonnegative unitriangular matrix into nonnegative resolution data. The subdivision operator $X^n \mapsto P_n$ sends each row of the resolution to an interlacing sequence, and interlacing is preserved under the nonnegative combinations that assemble the chain polynomials.

References

P. Brändén and L. Saud Maia Leite, “Totally nonnegative matrices, chain enumeration and zeros of polynomials,” arXiv:2412.06595 (2024).

Definitions

  • Chain polynomials

    RealRooted.BrandenLeite.chainPolynomialsource
    def chainPolynomial {R : Type*} [Semiring R] (A : LowerTriangularMatrix R) : ℕ → R[X]
  | 0 => 1
  | n + 1 =>
      X * ∑ k : Fin (n + 1), C (A (n + 1) k) * chainPolynomial A k
termination_by n => n
decreasing_by exact k.isLt

  • Resolvable matrix

    RealRooted.BrandenLeite.IsResolvablesource
    def IsResolvable {S : Type*} [CommSemiring S] [LE S]
    (R : LowerTriangularMatrix S) : Prop :=
  Nonempty (Resolution R)

  • Rows of 1 / (1 - x h(z))

    RealRooted.BrandenLeite.compositionRowsource
    def compositionRow {R : Type*} [CommSemiring R]
    (h : PowerSeries R) (n : ℕ) : R[X] :=
  ∑ k ∈ Finset.range (n + 1),
    C (PowerSeries.coeff n (h ^ k)) * X ^ k

  • Rows of g / (1 - x g h)

    RealRooted.BrandenLeite.twoKernelRowsource
    def twoKernelRow {R : Type*} [CommSemiring R]
    (g h : PowerSeries R) (n : ℕ) : R[X] :=
  ∑ k ∈ Finset.range (n + 1),
    C (PowerSeries.coeff n (g ^ (k + 1) * h ^ k)) * X ^ k

Theorems

  • Consecutive chain polynomials interlace

    RealRooted.BrandenLeite.interl_chainPolynomial_succ_of_isTotallyNonnegsource
    theorem interl_chainPolynomial_succ_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular R)
    (hR : Matrix.IsTotallyNonneg R) (n : ℕ) :
    Interl (chainPolynomial R n) (chainPolynomial R (n + 1))

  • Zeros of chain polynomials lie in [-1, 0]

    RealRooted.BrandenLeite.roots_chainPolynomial_mem_Icc_of_isTotallyNonnegsource
    theorem roots_chainPolynomial_mem_Icc_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular R)
    (hR : Matrix.IsTotallyNonneg R) (n : ℕ) :
    ∀ x ∈ (chainPolynomial R n).roots, x ∈ Set.Icc (-1) 0

  • Chain polynomials have nonnegative coefficients

    RealRooted.BrandenLeite.chainPolynomial_hasNonnegCoeffs_of_isTotallyNonnegsource
    theorem chainPolynomial_hasNonnegCoeffs_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular R)
    (hR : Matrix.IsTotallyNonneg R) (n : ℕ) :
    HasNonnegCoeffs (chainPolynomial R n)

  • Resolvable if and only if totally nonnegative

    RealRooted.BrandenLeite.isResolvable_iff_lowerUnitriangular_and_isTotallyNonnegsource
    theorem isResolvable_iff_lowerUnitriangular_and_isTotallyNonneg
    {R : LowerTriangularMatrix ℝ} :
    IsResolvable R ↔
      LowerTriangularMatrix.IsLowerUnitriangular R ∧
        Matrix.IsTotallyNonneg R

  • Positive constant diagonal

    RealRooted.BrandenLeite.chainPolynomial_isPFPolynomial_of_pos_constantDiagonalsource
    theorem chainPolynomial_isPFPolynomial_of_pos_constantDiagonal
    {δ : ℝ} {A : LowerTriangularMatrix ℝ} (hδ : 0 < δ)
    (hlower : LowerTriangularMatrix.IsLowerTriangular A)
    (hdiag : ∀ n, A n n = δ) (hA : Matrix.IsTotallyNonneg A) (n : ℕ) :
    IsPFPolynomial (chainPolynomial A n)

  • Rows of 1 / (1 - x h(z)) are PF and interlace

    RealRooted.BrandenLeite.compositionRows_mk_pf_and_interl_of_zerosource
    theorem compositionRows_mk_pf_and_interl_of_zero
    {f : ℕ → ℝ} (hf : IsPolyaFreqSeq f) (hf0 : f 0 = 0) :
    (∀ n, IsPFPolynomial (compositionRow (PowerSeries.mk f) n)) ∧
      ∀ n, Interl (compositionRow (PowerSeries.mk f) n)
        (compositionRow (PowerSeries.mk f) (n + 1))

  • Rows of g / (1 - x g h) are PF and interlace

    RealRooted.BrandenLeite.twoKernelRows_pf_and_interlsource
    theorem twoKernelRows_pf_and_interl
    {g h : ℕ → ℝ} (hg : IsPolyaFreqSeq g) (hh : IsPolyaFreqSeq h)
    (hg0 : 0 < g 0) (hh0 : h 0 = 0) :
    (∀ n, IsPFPolynomial
        (twoKernelRow (PowerSeries.mk g) (PowerSeries.mk h) n)) ∧
      ∀ n, Interl
        (twoKernelRow (PowerSeries.mk g) (PowerSeries.mk h) n)
        (twoKernelRow (PowerSeries.mk g) (PowerSeries.mk h) (n + 1))

  • Rows of 1 / (1 - x z (1+z)^d)

    RealRooted.BrandenLeite.binomialCompositionRows_pf_and_interlsource
    theorem binomialCompositionRows_pf_and_interl (d : ℕ) :
    (∀ n, IsPFPolynomial
      (compositionRow (PowerSeries.mk (binomialCompositionKernel d)) n)) ∧
      ∀ n, Interl
        (compositionRow (PowerSeries.mk (binomialCompositionKernel d)) n)
        (compositionRow
          (PowerSeries.mk (binomialCompositionKernel d)) (n + 1))

  • Rows of 1 / (1 - x z / (1-z)^e)

    RealRooted.BrandenLeite.inversePowerCompositionRows_pf_and_interlsource
    theorem inversePowerCompositionRows_pf_and_interl (e : ℕ) :
    (∀ n, IsPFPolynomial
      (compositionRow
        (PowerSeries.mk (inversePowerCompositionKernel e)) n)) ∧
      ∀ n, Interl
        (compositionRow
          (PowerSeries.mk (inversePowerCompositionKernel e)) n)
        (compositionRow
          (PowerSeries.mk (inversePowerCompositionKernel e)) (n + 1))

  • Planar networks from Whitney elimination

    RealRooted.BrandenLeite.networkMatrix_resolutionLambda_eqsource
    theorem networkMatrix_resolutionLambda_eq
    (R : LowerTriangularMatrix ℝ)
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular R)
    (hR : Matrix.IsTotallyNonneg R) :
    networkMatrix (resolutionLambda R) = R

  • Tiling polynomials of weighted lower shifts are PF

    RealRooted.BrandenLeite.weightedShiftTilingRow_separated_isPFPolynomialsource
    theorem weightedShiftTilingRow_separated_isPFPolynomial
    {b : ℕ → ℝ} (hb : ∀ n, 0 ≤ b n)
    {alphas : List ℝ} (halphas : ∀ a ∈ alphas, 0 ≤ a)
    {w : ℕ → ℝ} (hw : ∀ n, 0 ≤ w n)
    (N : ℕ) {r : ℕ} (hr : 0 < r) (i : Fin (N + 1)) :
    IsPFPolynomial
      (weightedShiftTilingRow b (alphas.map fun a n => a * w n) N r i)

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