Theorems

Rook polynomials

Weighted rook polynomials are weighted matching polynomials of complete bipartite graphs. For every nonnegative finite matrix they are real-rooted, with nonpositive roots; Nijenhuis’s signed normalization has nonnegative roots.

References

A. Nijenhuis, “On permanents and the zeros of rook polynomials,” Journal of Combinatorial Theory, Series A 21 (1976), 240–244. See also the rook-polynomial overview on symmetricfunctions.com.

Definitions

  • Rook placement

    RealRooted.Rook.IsRookPlacementsource
    def IsRookPlacement (P : Finset (Row × Column)) : Prop :=
  ∀ ⦃x⦄, x ∈ P → ∀ ⦃y⦄, y ∈ P → x ≠ y →
    x.1 ≠ y.1 ∧ x.2 ≠ y.2

  • Weighted rook polynomial

    RealRooted.Rook.weightedRookPolynomialsource
    def weightedRookPolynomial [Fintype Row] [Fintype Column]
    [DecidableEq Row] [DecidableEq Column]
    (A : Row → Column → ℝ) : ℝ[X] := by
  classical
  exact ∑ P ∈ (Finset.univ.filter fun P : Finset (Row × Column) ↦
      IsRookPlacement P),
    (∏ x ∈ P, C (A x.1 x.2)) * X ^ P.card

  • Nijenhuis's signed rook polynomial

    RealRooted.Rook.nijenhuisRookPolynomialsource
    def nijenhuisRookPolynomial [Fintype Row] [Fintype Column]
    [DecidableEq Row] [DecidableEq Column]
    (A : Row → Column → ℝ) : ℝ[X] :=
  (weightedRookPolynomial A).comp (-X)

Theorems

  • Rook polynomials are bipartite matching polynomials

    RealRooted.Challenges.Nijenhuis.bipartiteMatchingIdentitysource
    theorem bipartiteMatchingIdentity {Row : Type u} {Column : Type v}
    [Fintype Row] [Fintype Column] [DecidableEq Row] [DecidableEq Column]
    (A : Row → Column → ℝ) :
    Rook.weightedRookPolynomial A =
      Graph.weightedMatchingPolynomialByEdges
        (_root_.completeBipartiteGraph Row Column)
        (Rook.matrixEdgeWeight A)

  • Weighted rook polynomials are real-rooted

    RealRooted.Challenges.Nijenhuis.weightedRealRootedsource
    theorem weightedRealRooted {Row : Type u} {Column : Type v}
    [Fintype Row] [Fintype Column] [DecidableEq Row] [DecidableEq Column]
    (A : Row → Column → ℝ) (hA : ∀ r c, 0 ≤ A r c) :
    (Rook.weightedRookPolynomial A).Splits

  • The signed rook polynomial has nonnegative roots

    RealRooted.Challenges.Nijenhuis.signedRoots_nonnegativesource
    theorem signedRoots_nonnegative {Row : Type u} {Column : Type v}
    [Fintype Row] [Fintype Column] [DecidableEq Row] [DecidableEq Column]
    (A : Row → Column → ℝ) (hA : ∀ r c, 0 ≤ A r c) :
    ∀ z ∈ (Rook.nijenhuisRookPolynomial A).roots, 0 ≤ z

  • Rook polynomials of boards are real-rooted

    RealRooted.Challenges.Nijenhuis.ordinaryRealRootedsource
    theorem ordinaryRealRooted {Row : Type u} {Column : Type v}
    [Fintype Row] [Fintype Column] [DecidableEq Row] [DecidableEq Column]
    (B : Finset (Row × Column)) :
    (Rook.rookPolynomial B).Splits

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