q-Binomial coefficients and Theorem 6.6

Main results

• QBinomial.qBinom_pascal — Lemma 6.5: the q-binomial Pascal recurrence.
• QBinomial.rankGenPoly_eq_qBinom — Theorem 6.6: the rank-generating polynomial of L(m,n) equals [m+n choose m]_q.

References

• Stanley, Algebraic Combinatorics, Chapter 6.

noncomputable def QBinomial.qNumber (n : ℕ) : Polynomial ℤ

The q-analogue of a natural number: [n]_q = 1 + q + q² + ⋯ + q^{n-1}.

noncomputable def QBinomial.qFactorial : ℕ → Polynomial ℤ

The q-factorial: [n]!_q = [1]_q · [2]_q · ⋯ · [n]_q.

noncomputable def QBinomial.qBinom : ℕ → ℕ → Polynomial ℤ

The q-binomial coefficient [k choose j]_q, defined recursively via the Pascal recurrence.

@[simp]

theorem QBinomial.qBinom_zero_zero : qBinom 0 0 = 1

@[simp]

theorem QBinomial.qBinom_zero_succ (j : ℕ) : qBinom 0 (j + 1) = 0

@[simp]

theorem QBinomial.qBinom_succ_zero (k : ℕ) : qBinom (k + 1) 0 = 1

@[simp]

theorem QBinomial.qBinom_zero_right (k : ℕ) : qBinom k 0 = 1

theorem QBinomial.qBinom_succ_succ_of_le (k j : ℕ) (h : j ≤ k) : qBinom (k + 1) (j + 1) = qBinom k (j + 1) + Polynomial.X ^ (k - j) * qBinom k j

theorem QBinomial.qBinom_succ_succ_of_gt (k j : ℕ) (h : k < j) : qBinom (k + 1) (j + 1) = 0

theorem QBinomial.qBinom_eq_zero_of_lt {k j : ℕ} (h : k < j) : qBinom k j = 0

@[simp]

theorem QBinomial.qBinom_self (k : ℕ) : qBinom k k = 1

theorem QBinomial.qBinom_pascal (k j : ℕ) (hk : 1 ≤ k) (hj : 1 ≤ j) (hjk : j ≤ k) : qBinom k j = qBinom (k - 1) j + Polynomial.X ^ (k - j) * qBinom (k - 1) (j - 1)

Lemma 6.5 (q-binomial Pascal recurrence).

theorem QBinomial.qBinom_initial_zero : qBinom 0 0 = 1

theorem QBinomial.qBinom_eq_zero_of_gt {k j : ℕ} (h : j > k) : qBinom k j = 0

Rank-generating polynomial and Theorem 6.6

noncomputable def QBinomial.rankGenPoly (m n : ℕ) : Polynomial ℤ

The rank-generating polynomial of L(m,n): F(L(m,n)) = ∑_{λ ∈ L(m,n)} q^{|λ|} where |λ| is the sum of parts.

theorem QBinomial.rankGenPoly_zero_left (n : ℕ) : rankGenPoly 0 n = 1

theorem QBinomial.rankGenPoly_zero_right (m : ℕ) : rankGenPoly m 0 = 1

theorem QBinomial.rankGenPoly_succ_succ (m n : ℕ) : rankGenPoly (m + 1) (n + 1) = rankGenPoly (m + 1) n + Polynomial.X ^ (n + 1) * rankGenPoly m (n + 1)

The rank-generating polynomial recurrence from the first-part decomposition.

theorem QBinomial.qBinom_recurrence (m n : ℕ) : qBinom (m + 1 + (n + 1)) (m + 1) = qBinom (m + 1 + n) (m + 1) + Polynomial.X ^ (n + 1) * qBinom (m + (n + 1)) m

theorem QBinomial.rankGenPoly_eq_qBinom (m n : ℕ) : rankGenPoly m n = qBinom (m + n) m

Theorem 6.6. The rank-generating polynomial of L(m,n) equals [m+n choose m]_q.