q-Binomial Coefficients: Basic Definitions and Properties

This file introduces q-binomial coefficients (also known as Gaussian binomial coefficients) and their basic properties. The q-binomial coefficient ⟦n;k⟧_q is a polynomial in q that serves as a q-analogue of the ordinary binomial coefficient.

This file provides the canonical definition of q-binomial coefficients for this project.

Main Definitions

• qInt: The q-integer [n]_q = 1 + q + q^2 + ... + q^(n-1) (Definition 11.3.1)
• qFactorial: The q-factorial [n]_q! = [1]_q * [2]_q * ... * [n]_q (Definition 11.3.1)
• qBinomial: The q-binomial coefficient ⟦n;k⟧_q (Definition 11.2.1) — canonical definition
• qBinomialPoly: The q-binomial coefficient as a polynomial in ℤ[X]
• monotoneFunctions: The set of monotone functions from Fin k to Fin (m + 1)

Main Results

• qBinomial_eq_sum_increasing_tuples: Definition as sum over weakly increasing tuples (Proposition 11.2.1(a))
• qBinomial_eq_partition_gf: Equivalence to partition generating function (Definition 11.2.1(a))
• qBinomial_eq_sum_subsets: Alternative expression as sum over subsets (Proposition 11.2.1(b)) -- Proved in AlgebraicCombinatorics/Partitions/QBinomialFormulas.lean
• qBinomial_one_eq_binomial: At q=1, we recover ordinary binomial coefficients (Proposition 11.2.1(c))
• qBinomial_zero_of_lt: q-binomial is zero when k > n (Proposition 11.2.2)
• qBinomial_n_zero: ⟦n;0⟧_q = 1 (Proposition 11.2.3)
• qBinomial_n_n: ⟦n;n⟧_q = 1 (Proposition 11.2.3)
• qBinomial_rec_left: Recurrence ⟦n;k⟧_q = q^(n-k) * ⟦n-1;k-1⟧_q + ⟦n-1;k⟧_q (for 0 < k) (Theorem 11.2.4(a))
• qBinomial_rec_right: Recurrence ⟦n;k⟧_q = ⟦n-1;k-1⟧_q + q^k * ⟦n-1;k⟧_q (for 0 < k) (Theorem 11.2.4(b))
• qBinomial_quot_formula: Product formula for q-binomial (Theorem thm.pars.qbinom.quot1(a))
• qBinomial_eq_prod_quot: Quotient formula for q-binomial (Theorem thm.pars.qbinom.quot1(b))
• qInt_eq_geom_sum: [n]_q = (1 - q^n) / (1 - q) (Remark 11.3.2)
• qBinomial_eq_qFactorial_quot: ⟦n;k⟧_q = [n]_q! / ([k]_q! * [n-k]_q!) (Theorem 11.2.6)
• qBinomial_symm: Symmetry ⟦n;k⟧_q = ⟦n;n-k⟧_q (Proposition 11.2.7)
• card_partitions_with_parts_and_largest: Counting partitions (Proposition 11.1.1)

Implementation Notes

The q-binomial coefficient is defined via the sum over monotone tuples (Proposition 11.2.1(a)): ⟦n;k⟧_q = ∑_{0 ≤ i₁ ≤ i₂ ≤ ... ≤ iₖ ≤ n-k} q^(i₁ + i₂ + ... + iₖ)

This is equivalent to the generating function for partitions fitting in a k × (n-k) box (Definition 11.2.1(a)), but the monotone tuple formulation is more directly computable and avoids the need to sum over partitions of varying sizes.

We work over a general commutative semiring R with an element q, though the polynomial version over ℤ[q] is the primary object of interest.

Equivalent Formulations

The q-binomial coefficient has several equivalent definitions:

1. Monotone function sum (this definition): ∑_{f monotone} q^(∑ᵢ f(i)) See qBinomial_eq_sum_increasing_tuples.

2. Subset sum formula: ∑_{S ⊆ [n], |S|=k} q^(sum(S) - (1+2+...+k)) See qBinomial_eq_sum_subsets in Partitions/QBinomialFormulas.lean.

3. q-Pascal recurrence: [n;k]_q = [n-1;k-1]_q + q^k · [n-1;k]_q See qBinomial_rec_right (and qBinomial_rec_left for the dual form).

4. q-factorial quotient: [n]_q! / ([k]_q! · [n-k]_q!) See qBinomial_eq_qFactorial_quot.

Note: The file Partitions/QBinomialFormulas.lean defines equivalent versions of qBinomial using the q-Pascal recurrence in the sub-namespace AlgebraicCombinatorics.QBinomialRec. The file SignedCounting/AlternatingSums.lean defines a local version as Polynomial ℤ in the namespace AlgebraicCombinatorics.SignedCounting. Both are proven equivalent to this canonical definition via the theorems listed above.

References

• Darij Grinberg, Algebraic Combinatorics, Section 11.2-11.3
• [Kac-Cheung, Quantum Calculus, Chapters 5-7]
• [Stanley, Enumerative Combinatorics Vol. 1]

Tags

q-binomial, Gaussian binomial coefficient, q-integer, q-factorial, partition

q-Integers and q-Factorials

def AlgebraicCombinatorics.qInt {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : R

The q-integer [n]_q = 1 + q + q^2 + ... + q^(n-1). This is a q-analogue of the natural number n, since [n]_1 = n.

See Definition 11.3.1(a) in the source.

Equations

• AlgebraicCombinatorics.qInt n q = ∑ i ∈ Finset.range n, q ^ i

def AlgebraicCombinatorics.qFactorial {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : R

The q-factorial [n]_q! = [1]_q * [2]_q * ... * [n]_q. This is a q-analogue of n!, since [n]_1! = n!.

See Definition 11.3.1(b) in the source.

Equations

• AlgebraicCombinatorics.qFactorial n q = ∏ i ∈ Finset.range n, AlgebraicCombinatorics.qInt (i + 1) q

@[simp]

theorem AlgebraicCombinatorics.qInt_zero {R : Type u_1} [CommSemiring R] (q : R) : qInt 0 q = 0

@[simp]

theorem AlgebraicCombinatorics.qInt_one {R : Type u_1} [CommSemiring R] (q : R) : qInt 1 q = 1

@[simp]

theorem AlgebraicCombinatorics.qInt_two {R : Type u_1} [CommSemiring R] (q : R) : qInt 2 q = 1 + q

theorem AlgebraicCombinatorics.qInt_succ {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : qInt (n + 1) q = qInt n q + q ^ n

@[simp]

theorem AlgebraicCombinatorics.qInt_one_eq {R : Type u_1} [CommSemiring R] (n : ℕ) : qInt n 1 = ↑n

The q-integer satisfies [n]_1 = n. See Remark 11.3.2 in the source.

@[simp]

theorem AlgebraicCombinatorics.qFactorial_zero {R : Type u_1} [CommSemiring R] (q : R) : qFactorial 0 q = 1

@[simp]

theorem AlgebraicCombinatorics.qFactorial_one {R : Type u_1} [CommSemiring R] (q : R) : qFactorial 1 q = 1

theorem AlgebraicCombinatorics.qFactorial_succ {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : qFactorial (n + 1) q = qFactorial n q * qInt (n + 1) q

@[simp]

theorem AlgebraicCombinatorics.qFactorial_one_eq {R : Type u_1} [CommSemiring R] (n : ℕ) : qFactorial n 1 = ↑n.factorial

The q-factorial satisfies [n]_1! = n!. See Remark 11.3.2 in the source.

theorem AlgebraicCombinatorics.qInt_eq_geom_sum {R : Type u_2} [CommRing R] (n : ℕ) (q : R) : (1 - q) * qInt n q = 1 - q ^ n

The q-integer as a rational function: [n]_q = (1 - q^n) / (1 - q). This holds in any ring where 1 - q is invertible, or as formal power series.

See Remark 11.3.2 in the source.

theorem AlgebraicCombinatorics.qFactorial_split {R : Type u_1} [CommSemiring R] (n k : ℕ) (hk : k ≤ n) (q : R) : qFactorial n q = (∏ i ∈ Finset.range k, qInt (n - i) q) * qFactorial (n - k) q

Helper: qFactorial n = (∏ i ∈ range k, qInt (n - i) q) * qFactorial (n - k) when k ≤ n.

This is the key splitting lemma for the factorial form of the q-binomial coefficient. It states that [n]_q! can be split as: [n]_q! = [n]_q · [n-1]_q · ... · [n-k+1]_q · [n-k]_q!

theorem AlgebraicCombinatorics.qInt_ne_zero {R : Type u_2} [Field R] (n : ℕ) (q : R) (hq : q ^ n ≠ 1) : qInt n q ≠ 0

qInt n q ≠ 0 when q^n ≠ 1 (i.e., when q is not an n-th root of unity).

theorem AlgebraicCombinatorics.qFactorial_ne_zero {R : Type u_2} [Field R] (n : ℕ) (q : R) (hq : ∀ i ∈ Finset.range n, q ^ (i + 1) ≠ 1) : qFactorial n q ≠ 0

qFactorial n q ≠ 0 when q^i ≠ 1 for i = 1, ..., n.

q-Binomial Coefficients

def AlgebraicCombinatorics.PartitionFitsInBox (n k m : ℕ) (μ : n.Partition) : Prop

A partition fits in a k × m box if it has at most k parts, each of size at most m.

Equations

• AlgebraicCombinatorics.PartitionFitsInBox n k m μ = (μ.parts.card ≤ k ∧ ∀ p ∈ μ.parts, p ≤ m)

def AlgebraicCombinatorics.monotoneFunctions (k m : ℕ) : Finset (Fin k → Fin (m + 1))

The set of monotone functions from Fin k to Fin (m + 1), representing weakly increasing k-tuples with entries in {0, 1, ..., m}.

Equations

• AlgebraicCombinatorics.monotoneFunctions k m = {f : Fin k → Fin (m + 1) | Monotone f}

noncomputable def AlgebraicCombinatorics.qBinomial {R : Type u_1} [CommSemiring R] (n k : ℕ) (q : R) : R

The q-binomial coefficient ⟦n;k⟧_q, defined via the sum over monotone tuples: ⟦n;k⟧_q = ∑_{0 ≤ i₁ ≤ i₂ ≤ ... ≤ iₖ ≤ n-k} q^(i₁ + i₂ + ... + iₖ)

This is equivalent to the generating function for partitions fitting in a k × (n-k) box (see qBinomial_eq_partition_gf).

See Definition 11.2.1(a) and Proposition 11.2.1(a) in the source.

Equations

• AlgebraicCombinatorics.qBinomial n k q = if k ≤ n then ∑ f ∈ AlgebraicCombinatorics.monotoneFunctions k (n - k), q ^ ∑ i : Fin k, ↑(f i) else 0

noncomputable def AlgebraicCombinatorics.qBinomialPoly (n k : ℕ) : Polynomial ℤ

The q-binomial coefficient as a polynomial in ℤ[X].

This is the generating function for partitions fitting in a k × (n-k) box: ⟦n;k⟧_q = ∑_{λ fits in k × (n-k) box} q^|λ|

See Definition 11.2.1(a) in the source.

Equations

• AlgebraicCombinatorics.qBinomialPoly n k = if k ≤ n then ∑ f ∈ AlgebraicCombinatorics.monotoneFunctions k (n - k), Polynomial.X ^ ∑ i : Fin k, ↑(f i) else 0

Alternative Characterizations

theorem AlgebraicCombinatorics.qBinomial_eq_sum_increasing_tuples {R : Type u_1} [CommSemiring R] (n k : ℕ) (hk : k ≤ n) (q : R) : qBinomial n k q = ∑ f ∈ monotoneFunctions k (n - k), q ^ ∑ i : Fin k, ↑(f i)

The q-binomial is defined as a sum over weakly increasing tuples: ⟦n;k⟧_q = ∑_{0 ≤ i₁ ≤ i₂ ≤ ... ≤ iₖ ≤ n-k} q^(i₁ + i₂ + ... + iₖ)

This is the definition, restated for clarity.

See Proposition 11.2.1(a) in the source.

def AlgebraicCombinatorics.partitionsInBox (n k m : ℕ) : Finset n.Partition

The set of partitions of n fitting in a k × m box.

Argument order: This definition uses (n k m : ℕ) where:

• n is the partition size
• k is the maximum number of parts (length ≤ k)
• m is the maximum part size (largest part ≤ m)

This is the canonical definition of partitionsInBox for this project. The definition QBinomialRec.partitionsInBox in QBinomialFormulas.lean uses the same argument order.

Equations

• AlgebraicCombinatorics.partitionsInBox n k m = {μ : n.Partition | μ.parts.card ≤ k ∧ ∀ p ∈ μ.parts, p ≤ m}

theorem AlgebraicCombinatorics.card_monotoneFunctions_sum_eq (k m s : ℕ) (_hs : s ≤ k * m) : {f ∈ monotoneFunctions k m | ∑ i : Fin k, ↑(f i) = s}.card = (partitionsInBox s k m).card

The key bijection lemma: for each s, the number of monotone functions with sum s equals the number of partitions of s fitting in a k × m box.

This follows from the classical bijection between monotone functions and partitions:

• Forward: f ↦ partition whose parts are the nonzero values of f
• Backward: μ ↦ monotone function obtained by padding μ.parts to k values and sorting

This is equivalent to the stars-and-bars / lattice path correspondence.

theorem AlgebraicCombinatorics.qBinomial_eq_partition_gf {R : Type u_1} [CommSemiring R] (n k : ℕ) (hk : k ≤ n) (q : R) : qBinomial n k q = ∑ m ∈ Finset.range (k * (n - k) + 1), (partitionsInBox m k (n - k)).card • q ^ m

The q-binomial coefficient equals the generating function for partitions fitting in a k × (n-k) box.

Note: This requires k ≤ n because when k > n, the LHS is 0 by definition but the RHS would count the empty partition (giving 1). In the mathematical definition over ℤ, when k > n, n - k < 0, so no partition has largest part ≤ n - k. But in Lean with ℕ subtraction, n - k = 0 when k > n, and the empty partition vacuously satisfies "all parts ≤ 0".

See Definition 11.2.1(a) in the source.

Basic Properties

Helper definitions and lemmas for counting monotone functions

@[simp]

theorem AlgebraicCombinatorics.qBinomial_one_eq_binomial {R : Type u_1} [CommSemiring R] (n k : ℕ) : qBinomial n k 1 = ↑(n.choose k)

At q = 1, the q-binomial coefficient equals the ordinary binomial coefficient.

See Proposition 11.2.1(c) in the source.

@[simp]

theorem AlgebraicCombinatorics.qBinomial_zero_of_lt {R : Type u_1} [CommSemiring R] (n k : ℕ) (hk : n < k) (q : R) : qBinomial n k q = 0

The q-binomial coefficient is zero when k > n.

See Proposition 11.2.2 in the source.

@[simp]

theorem AlgebraicCombinatorics.qBinomial_n_zero {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : qBinomial n 0 q = 1

⟦n;0⟧_q = 1 for all n.

See Proposition 11.2.3 in the source.

@[simp]

theorem AlgebraicCombinatorics.qBinomial_n_n {R : Type u_1} [CommSemiring R] (n : ℕ) (q : R) : qBinomial n n q = 1

⟦n;n⟧_q = 1 for all n.

See Proposition 11.2.3 in the source.

Recurrence Relations

theorem AlgebraicCombinatorics.qBinomial_rec_left {R : Type u_1} [CommSemiring R] (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : 0 < k) (q : R) : qBinomial n k q = q ^ (n - k) * qBinomial (n - 1) (k - 1) q + qBinomial (n - 1) k q

First recurrence relation for q-binomial coefficients: ⟦n;k⟧_q = q^(n-k) * ⟦n-1;k-1⟧_q + ⟦n-1;k⟧_q

This is a q-analogue of Pascal's identity.

Note: The hypothesis 0 < k is necessary because in Lean with k : ℕ, we have k - 1 = 0 when k = 0 due to saturating subtraction. This would make the RHS equal to q^n * qBinomial (n-1) 0 q + qBinomial (n-1) 0 q = q^n + 1, which is not equal to qBinomial n 0 q = 1 in general.

See Theorem 11.2.4(a) in the source. The source handles k ∈ ℤ with the convention that (n choose k)_q = 0 for negative k, and explicitly notes that when k = 0, the identity reduces to 1 = q^(n-k) * 0 + 1.

Transpose of monotone functions

The following helper definitions and lemmas establish a bijection between monotone functions Fin k → Fin (m + 1) and Fin m → Fin (k + 1) via transposition. This is used to prove the symmetry of q-binomial coefficients.

theorem AlgebraicCombinatorics.transposeMonotone_involutive (k m : ℕ) (f : Fin k → Fin (m + 1)) (hf : Monotone f) : AlgebraicCombinatorics.transposeMonotone✝ m k (AlgebraicCombinatorics.transposeMonotone✝¹ k m f) = f

theorem AlgebraicCombinatorics.sum_transposeMonotone (k m : ℕ) (f : Fin k → Fin (m + 1)) : ∑ j : Fin m, ↑(AlgebraicCombinatorics.transposeMonotone✝ k m f j) = ∑ i : Fin k, ↑(f i)

theorem AlgebraicCombinatorics.qBinomial_rec_right {R : Type u_1} [CommSemiring R] (n : ℕ) (hn : 0 < n) (k : ℕ) (hk : 0 < k) (q : R) : qBinomial n k q = qBinomial (n - 1) (k - 1) q + q ^ k * qBinomial (n - 1) k q

Second recurrence relation for q-binomial coefficients: ⟦n;k⟧_q = ⟦n-1;k-1⟧_q + q^k * ⟦n-1;k⟧_q

This is another q-analogue of Pascal's identity.

Note: The hypothesis 0 < k is necessary because in Lean with k : ℕ, we have k - 1 = 0 when k = 0 due to saturating subtraction. This would make the RHS equal to qBinomial (n-1) 0 q + q^0 * qBinomial (n-1) 0 q = 1 + 1 = 2, which is not equal to qBinomial n 0 q = 1.

See Theorem 11.2.4(b) in the source. The source handles k ∈ ℤ with the convention that (n choose k)_q = 0 for negative k.

Product Formulas

theorem AlgebraicCombinatorics.qBinomial_quot_formula {R : Type u_2} [CommRing R] (n k : ℕ) (hk : k ≤ n) (q : R) : (∏ i ∈ Finset.range k, (1 - q ^ (i + 1))) * qBinomial n k q = ∏ i ∈ Finset.range k, (1 - q ^ (n - i))

Product formula for q-binomial coefficients (polynomial identity): (1-q^k)(1-q^(k-1))...(1-q) * ⟦n;k⟧_q = (1-q^n)(1-q^(n-1))...(1-q^(n-k+1))

This is Theorem thm.pars.qbinom.quot1 part (a) from the source. Also known as Theorem 11.2.5(a) in the section numbering.

The identity holds over any commutative ring without requiring any divisibility conditions. This is the "polynomial form" that avoids fractions, making it easier to substitute values for q without worrying about whether denominators are invertible.

theorem AlgebraicCombinatorics.qBinomial_eq_prod_quot {R : Type u_2} [Field R] (n k : ℕ) (hk : k ≤ n) (q : R) (hq : ∀ i ∈ Finset.range k, q ^ (i + 1) ≠ 1) : qBinomial n k q = ∏ i ∈ Finset.range k, (1 - q ^ (n - i)) / (1 - q ^ (i + 1))

Product formula for q-binomial coefficients (quotient form): ⟦n;k⟧_q = ∏_{i=0}^{k-1} (1-q^(n-i)) / (1-q^(i+1))

This is Theorem thm.pars.qbinom.quot1 part (b) from the source. Also known as Theorem 11.2.5(b) in the section numbering.

This holds in any ring where the denominator is invertible. The hypothesis hq ensures that q is not a root of unity of order ≤ k, which guarantees all factors (1 - q^(i+1)) in the denominator are nonzero.

Note: Part (b) is the more intuitive statement showing the q-binomial as a ratio of products, but part (a) (qBinomial_quot_formula) is easier to work with when substituting values for q since it has no denominators.

theorem AlgebraicCombinatorics.qBinomial_eq_qInt_prod_quot {R : Type u_2} [Field R] (n k : ℕ) (hk : k ≤ n) (q : R) (hq : ∀ i ∈ Finset.range k, q ^ (i + 1) ≠ 1) : qBinomial n k q = (∏ i ∈ Finset.range k, qInt (n - i) q) / qFactorial k q

q-binomial coefficient in terms of q-integers (falling factorial form): ⟦n;k⟧_q = [n]_q * [n-1]_q * ... * [n-k+1]_q / [k]_q!

See Theorem 11.2.6 in the source.

theorem AlgebraicCombinatorics.qBinomial_eq_qFactorial_quot {R : Type u_2} [Field R] (n k : ℕ) (hk : k ≤ n) (q : R) (hq : ∀ i ∈ Finset.range n, q ^ (i + 1) ≠ 1) : qBinomial n k q = qFactorial n q / (qFactorial k q * qFactorial (n - k) q)

q-binomial coefficient in terms of q-factorials: ⟦n;k⟧_q = [n]_q! / ([k]_q! * [n-k]_q!)

See Theorem 11.2.6 in the source. This is also Theorem thm.pars.qbinom.quot2 from the text.

theorem AlgebraicCombinatorics.qBinomial_symm {R : Type u_1} [CommSemiring R] (n k : ℕ) (hk : k ≤ n) (q : R) : qBinomial n k q = qBinomial n (n - k) q

Symmetry of q-binomial coefficients: ⟦n;k⟧_q = ⟦n;n-k⟧_q.

See Proposition 11.2.7 in the source.

Counting Partitions

def AlgebraicCombinatorics.monotoneFunctionsEquivSym (k ℓ : ℕ) : { f : Fin k → Fin (ℓ + 1) // Monotone f } ≃ Sym (Fin (ℓ + 1)) k

Equivalence between monotone functions Fin k → Fin (ℓ + 1) and multisets of size k over Fin (ℓ + 1). A monotone function is converted to a multiset by taking its values (with multiplicity), and a multiset is converted to a monotone function by sorting and indexing.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicCombinatorics.card_monotoneFunctions_eq_choose (k ℓ : ℕ) : (monotoneFunctions k ℓ).card = (k + ℓ).choose k

The number of partitions with at most k parts and largest part at most ℓ equals the number of monotone functions from Fin k to Fin (ℓ + 1), which is the binomial coefficient (k + ℓ) choose k.

This is a consequence of the bijection between such partitions and lattice paths from (0,0) to (ℓ,k) using east and north steps.

See discussion before Proposition 11.1.1 in the source.

theorem AlgebraicCombinatorics.card_partitions_with_parts_and_largest (k ℓ : ℕ) (hk : 0 < k) (hℓ : 0 < ℓ) : (monotoneFunctions (k - 1) (ℓ - 1)).card = (k + ℓ - 2).choose (k - 1)

The number of partitions with exactly k parts and largest part exactly ℓ equals the binomial coefficient (k + ℓ - 2) choose (k - 1).

This counts lattice paths from (0,0) to (ℓ,k) that start with an east step and end with a north step.

See Proposition 11.1.1 in the source.

Examples

Helper definitions for explicit enumeration of monotone functions

For small values of n and k, we can enumerate all monotone functions explicitly and compute the q-binomial polynomial by direct summation.