Chow polynomials of totally nonnegative matrices

For a lower-triangular matrix $A$, the Chow derangement polynomials $d_n$ satisfy a triangular recurrence driven by the rows of $A$. The Chow polynomials are

c_n = \sum_{k \leq n} A(n,k)\, d_k.

For the incidence data of a poset, these generalize the Chow polynomials of matroids and posets.

Theorem (Brändén–Vecchi, Theorem 4.18). If $A$ is lower unitriangular and totally nonnegative, then $c_n$ and $d_n$ have nonnegative coefficients and only real zeros. Moreover $c_n$ interlaces $c_{n+1}$, and $c_n$ interlaces $d_n$.

Further results:

Pólya frequency symbols: for the Toeplitz matrix of an Aissen–Schoenberg–Whitney–Edrei symbol $e^{\gamma z} \prod_i (1 + \alpha_i z) \big/ \prod_i (1 - \beta_i z)$ (Theorem 8.4), the Chow polynomials are PF polynomials and interlace consecutively. This also holds in the full projective form, with an outer scalar, a zero prefix and a shift.
Signed words: for finite supersymmetric symbols, the Chow polynomial equals a signed-word enumerator by descents and collisions (Theorem 8.11). It specializes to the Smirnov word polynomials.
Sharpness: a zero prefix of length three can destroy real-rootedness, even though the symbol remains a Pólya frequency sequence.

References

P. Brändén and L. Vecchi, “Chow polynomials of totally nonnegative matrices and posets” (2025). The resolution machinery comes from the Brändén–Saud Leite page.

Definitions

Chow derangement polynomials

RealRooted.BrandenVecchi.chowDerangementsource

def chowDerangement (A : LowerTriangularMatrix R) : ℕ → R[X]
  | 0 => 1
  | n + 1 =>
      X * Polynomial.chowS n (∑ k : Fin (n + 1),
        C (A (n + 1) k) * chowDerangement A k)
  termination_by n => n
  decreasing_by exact k.isLt

Chow polynomials of a lower-triangular matrix

RealRooted.BrandenVecchi.chowPolynomialsource

def chowPolynomial (A : LowerTriangularMatrix R) (n : ℕ) : R[X] :=
  ∑ k ∈ Finset.range (n + 1), C (A n k) * chowDerangement A k

Chow polynomials of a Pólya frequency symbol

RealRooted.BrandenVecchi.aswEdreiChowsource

def aswEdreiChow
    (gamma : ℝ) (alpha beta : ℕ → ℝ) (n : ℕ) : ℝ[X] :=
  chowPolynomial (aswEdreiToeplitz gamma alpha beta) n

Chow polynomials of a supersymmetric symbol

RealRooted.BrandenVecchi.finiteSupersymmetricChowsource

def finiteSupersymmetricChow (xs ys : List ℝ) (n : ℕ) : ℝ[X] :=
  chowPolynomial (finiteSupersymmetricToeplitz xs ys) n

Theorems

Chow polynomials have nonnegative coefficients

RealRooted.BrandenVecchi.chowPolynomial_nonnegCoeffs_of_isTotallyNonnegsource

theorem chowPolynomial_nonnegCoeffs_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular A)
    (hA : Matrix.IsTotallyNonneg A) (n : ℕ) :
    HasNonnegCoeffs (chowPolynomial A n)

Chow polynomials are real-rooted

RealRooted.BrandenVecchi.chowPolynomial_eq_zero_or_splits_of_isTotallyNonnegsource

theorem chowPolynomial_eq_zero_or_splits_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular A)
    (hA : Matrix.IsTotallyNonneg A) (n : ℕ) :
    chowPolynomial A n = 0 ∨ (chowPolynomial A n).Splits

Consecutive Chow polynomials interlace

RealRooted.BrandenVecchi.chowPolynomial_interl_succ_of_isTotallyNonnegsource

theorem chowPolynomial_interl_succ_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular A)
    (hA : Matrix.IsTotallyNonneg A) (n : ℕ) :
    Interl (chowPolynomial A n) (chowPolynomial A (n + 1))

c_n interlaces d_n

RealRooted.BrandenVecchi.chowPolynomial_interl_chowDerangement_of_isTotallyNonnegsource

theorem chowPolynomial_interl_chowDerangement_of_isTotallyNonneg
    (hunit : LowerTriangularMatrix.IsLowerUnitriangular A)
    (hA : Matrix.IsTotallyNonneg A) (n : ℕ) :
    Interl (chowPolynomial A n) (chowDerangement A n)

Pólya frequency symbols give PF Chow polynomials

RealRooted.BrandenVecchi.aswEdreiFullProjectiveChow_theoremsource

theorem aswEdreiFullProjectiveChow_theorem
    {outer gamma epsilon : ℝ} {N : ℕ} {alpha beta : ℕ → ℝ}
    (houter : 0 ≤ outer) (hgamma : 0 ≤ gamma)
    (halpha : ∀ i, 0 ≤ alpha i)
    (hbeta : ∀ i, 0 ≤ beta i)
    (hsum : Summable fun i => alpha i + beta i)
    (hepsilon : 0 ≤ epsilon) (n : ℕ) :
    IsPFPolynomial
        (aswEdreiFullProjectiveChow outer N gamma alpha beta epsilon n) ∧
      Interl
        (aswEdreiFullProjectiveChow outer N gamma alpha beta epsilon n)
        (aswEdreiFullProjectiveChow outer N gamma alpha beta epsilon
          (n + 1))

Chow polynomials as signed-word enumerators

RealRooted.BrandenVecchi.finiteSupersymmetricChow_eq_finiteSignedWordEnumeratorsource

theorem finiteSupersymmetricChow_eq_finiteSignedWordEnumerator
    (xs ys : List ℝ) (n : ℕ) :
    finiteSupersymmetricChow xs ys n =
      finiteSignedWordEnumerator xs ys n

Specialization to Smirnov word polynomials

RealRooted.BrandenVecchi.finiteSupersymmetricChow_replicate_one_nil_eq_smirnovsource

theorem finiteSupersymmetricChow_replicate_one_nil_eq_smirnov
    (m n : ℕ) :
    finiteSupersymmetricChow (List.replicate m (1 : ℝ)) [] n =
      weightedSmirnovPolynomial (fun _ : Fin m => (1 : ℝ)) n

A zero prefix of length three breaks real-rootedness

RealRooted.BrandenVecchi.chowPolynomial_three_zero_prefix_six_not_splitssource

theorem chowPolynomial_three_zero_prefix_six_not_splits :
    ¬(chowPolynomial
      (toeplitz (scaledZeroPrefix 1 3 (fun _ : ℕ => (1 : ℝ)))) 6).Splits

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

Chow polynomials of totally nonnegative matrices

References

≔ Definitions

⊢ Theorems

Definitions

Theorems