Domination in rook graphs

DefinitionRook graph#✓fully proved

For natural numbers \(n\) and \(m\), the rook graph on the \(n \times m\) board is the simple graph whose vertices are the cells \((i, j)\) with \(0 \le i < n\) and \(0 \le j < m\), in which two cells are adjacent if and only if they are distinct and lie in the same row (same \(i\)) or the same column (same \(j\)).

def rookGraph (n m : ℕ) : SimpleGraph (Fin n × Fin m) where
  Adj x y := x ≠ y ∧ (x.1 = y.1 ∨ x.2 = y.2)
  symm := ⟨by
    rintro x y ⟨hxy, h | h⟩
    · exact ⟨hxy.symm, Or.inl h.symm⟩
    · exact ⟨hxy.symm, Or.inr h.symm⟩⟩
  loopless := ⟨by
    intro x hx
    exact hx.1 rfl⟩

Used by 4

Used bySnort on the rook's graph · Snort on the \(2 \times 2\) queen's and rook's graphs · Dominating rook placements · Dominating sets of the rook graph

TheoremDominating sets of the rook graph#✓fully proved

For natural numbers \(n\) and \(m\), a finite set \(S\) of cells of the \(n \times m\) board dominates the rook graph on that board if and only if for every cell \((i, j)\), some cell of \(S\) lies in row \(i\) or some cell of \(S\) lies in column \(j\).

theorem rookGraph_isDominating_iff {n m : ℕ}
    {s : Finset (Fin n × Fin m)} :
    (rookGraph n m).IsDominating ↑s ↔
      ∀ i : Fin n, ∀ j : Fin m,
        (∃ j' : Fin m, (i, j') ∈ s) ∨ ∃ i' : Fin n, (i', j) ∈ s

Uses 2 · Used by 1

Statement usesDominating set · Rook graph

Used byDominating rook placements

DefinitionRook placements covering all rows and columns#✓fully proved

For natural numbers \(n\), \(m\) and \(k\), \(E_{n,m}(k)\) is the number of \(k\)-element sets of cells of the \(n \times m\) board that contain a cell in every row and a cell in every column (Mertens' \(E_{n,m}(k)\)).

def rookCoverCount (n m k : ℕ) : ℕ :=
  (((Finset.univ : Finset (Fin n × Fin m)).powersetCard k).filter
    (fun s => (∀ i : Fin n, ∃ j : Fin m, (i, j) ∈ s) ∧
      ∀ j : Fin m, ∃ i : Fin n, (i, j) ∈ s)).card

Used by 2

Used byRecursion for rook placements covering all rows and columns · Dominating rook placements via covering placements

DefinitionDominating rook placements#✓fully proved

For natural numbers \(n\), \(m\) and \(k\), \(d_{n,m}(k)\) is the number of \(k\)-element sets of cells of the \(n \times m\) board that are dominating sets of the rook graph on that board (Mertens' \(d_{R_{n,m}}(k)\)).

def rookDominatingCount (n m k : ℕ) : ℕ :=
  (((Finset.univ : Finset (Fin n × Fin m)).powersetCard k).filter
    (fun s : Finset (Fin n × Fin m) =>
      (SimpleGraph.rookGraph n m).IsDominating (s : Set (Fin n × Fin m)))).card

Uses 3 · Used by 3

Statement usesDominating set · Rook graph · Dominating sets of the rook graph

Used byDominating rook placements at high density · Dominating rook placements via covering placements · Domination polynomial of the rook graph

DefinitionDomination polynomial of the rook graph#✓fully proved

For natural numbers \(n\) and \(m\), the rook domination polynomial of the \(n \times m\) board is the integer polynomial \(D_{n,m}(x) = \sum_{k=0}^{nm} d_{n,m}(k)\, x^k\), where \(d_{n,m}(k)\) is the number of \(k\)-element sets of cells of the \(n \times m\) board that are dominating sets of the rook graph on that board.

noncomputable def rookDominationPolynomial (n m : ℕ) : Polynomial ℤ :=
  ∑ k ∈ Finset.range (n * m + 1),
    Polynomial.C (rookDominatingCount n m k : ℤ) * Polynomial.X ^ k

Uses 1 · Used by 2

Statement usesDominating rook placements

Used bySingle-sum formula for the rook domination polynomial · Symmetric formula for the rook domination polynomial

TheoremDominating rook placements via covering placements#●ready to prove

For natural numbers \(n, m \ge 1\) and \(k\), let \(d_{n,m}(k)\) be the number of \(k\)-element sets of cells of the \(n \times m\) board that are dominating sets of the rook graph on that board, and let \(E_{a,b}(k)\) be the number of \(k\)-element sets of cells of the \(a \times b\) board that contain a cell in every row and a cell in every column. Then

\[d_{n,m}(k) = \binom{nm}{k} - \sum_{r=1}^{n} \sum_{c=1}^{m} \binom{n}{r} \binom{m}{c} E_{n-r,m-c}(k).\]

theorem_wanted rookDominatingCount_eq_choose_sub_sum_rookCoverCount
    (n m k : ℕ) (hn : 0 < n) (hm : 0 < m) :
    (rookDominatingCount n m k : ℤ) =
      ((n * m).choose k : ℤ) -
        ∑ r ∈ Finset.Icc 1 n, ∑ c ∈ Finset.Icc 1 m,
          (n.choose r : ℤ) * (m.choose c : ℤ) *
            (rookCoverCount (n - r) (m - c) k : ℤ)

Sources

• Stephan Mertens, "Domination Polynomial of the Rook Graph", Theorem 1 (thm:R-E).

Uses 2

Statement usesRook placements covering all rows and columns · Dominating rook placements

TheoremRecursion for rook placements covering all rows and columns#●ready to prove

For natural numbers \(n, m \ge 1\) and \(k\), let \(E_{a,b}(k)\) denote the number of \(k\)-element sets of cells of the \(a \times b\) board that contain a cell in every row and a cell in every column. Then

\[E_{n,m}(k) = \binom{nm}{k} - \sum_{(r,c) \ne (0,0)} \binom{n}{r} \binom{m}{c} E_{n-r,m-c}(k),\]

where the sum runs over all pairs \((r, c) \ne (0, 0)\) with \(0 \le r \le n\) and \(0 \le c \le m\).

theorem_wanted rookCoverCount_eq_choose_sub_sum_rookCoverCount
    (n m k : ℕ) (hn : 0 < n) (hm : 0 < m) :
    (rookCoverCount n m k : ℤ) =
      ((n * m).choose k : ℤ) -
        ∑ r ∈ Finset.range (n + 1), ∑ c ∈ Finset.range (m + 1),
          (n.choose r : ℤ) * (m.choose c : ℤ) *
            (rookCoverCount (n - r) (m - c) k : ℤ) *
            (if r = 0 ∧ c = 0 then 0 else 1)

Sources

• Stephan Mertens, "Domination Polynomial of the Rook Graph", Theorem 2 (thm:E-recursion).

Uses 1

Statement usesRook placements covering all rows and columns

TheoremDominating rook placements at high density#●ready to prove

For natural numbers \(n, m \ge 1\) and \(k\) with \(k > nm - n - m - \min(n, m) + 2\), let \(d_{n,m}(k)\) be the number of \(k\)-element sets of cells of the \(n \times m\) board that are dominating sets of the rook graph on that board. Then

\[d_{n,m}(k) = \binom{nm}{k} - nm \binom{(n-1)(m-1)}{k}.\]

theorem_wanted rookDominatingCount_eq_choose_sub_mul_choose
    (n m k : ℕ) (hn : 0 < n) (hm : 0 < m)
    (hk : (n : ℤ) * m - n - m - (min n m : ℤ) + 2 < k) :
    (rookDominatingCount n m k : ℤ) =
      ((n * m).choose k : ℤ) -
        (n : ℤ) * m * (((n - 1) * (m - 1)).choose k : ℤ)

Sources

• Stephan Mertens, "Domination Polynomial of the Rook Graph", Corollary 3 (cor:high-density).

Uses 1

Statement usesDominating rook placements

TheoremSingle-sum formula for the rook domination polynomial#●ready to prove

For natural numbers \(n, m \ge 1\), the rook domination polynomial \(D_{n,m}(x)\) of the \(n \times m\) board, an integer polynomial, satisfies

\[D_{n,m}(x) = ((1+x)^n - 1)^m - (-1)^m \sum_{k=0}^{m-1} (-1)^k \binom{m}{k} ((1+x)^k - 1)^n.\]

theorem_wanted rookDominationPolynomial_eq
    (n m : ℕ) (hn : 0 < n) (hm : 0 < m) :
    rookDominationPolynomial n m =
      ((1 + Polynomial.X) ^ n - 1) ^ m -
        (-1 : Polynomial ℤ) ^ m *
          ∑ k ∈ Finset.range m,
            (-1 : Polynomial ℤ) ^ k * Polynomial.C (m.choose k : ℤ) *
              ((1 + Polynomial.X) ^ k - 1) ^ n

Sources

• Stephan Mertens, "Domination Polynomial of the Rook Graph", Theorem 4 (thm:domination-polynomial).

Uses 1

Statement usesDomination polynomial of the rook graph

TheoremSymmetric formula for the rook domination polynomial#●ready to prove

For natural numbers \(n, m \ge 1\), the rook domination polynomial \(D_{n,m}(x)\) of the \(n \times m\) board, an integer polynomial, satisfies

\[D_{n,m}(x) = ((1+x)^n - 1)^m + ((1+x)^m - 1)^n - (-1)^{n+m} \sum_{\ell=0}^{n} \sum_{k=0}^{m} (-1)^{k+\ell} \binom{n}{\ell} \binom{m}{k} (1+x)^{k\ell}.\]

theorem_wanted rookDominationPolynomial_eq_symmetric
    (n m : ℕ) (hn : 0 < n) (hm : 0 < m) :
    rookDominationPolynomial n m =
      ((1 + Polynomial.X) ^ n - 1) ^ m +
          ((1 + Polynomial.X) ^ m - 1) ^ n -
        (-1 : Polynomial ℤ) ^ (n + m) *
          ∑ ℓ ∈ Finset.range (n + 1), ∑ k ∈ Finset.range (m + 1),
            Polynomial.C ((n.choose ℓ : ℤ) * (m.choose k : ℤ)) *
              (-1 : Polynomial ℤ) ^ (k + ℓ) *
              (1 + Polynomial.X) ^ (k * ℓ)

Sources

• Stephan Mertens, "Domination Polynomial of the Rook Graph", Corollary 5 (cor:domination-polynomial).

Uses 1

Statement usesDomination polynomial of the rook graph

5 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.