q-Binomial Formulas

This file formalizes the q-binomial formulas from the Algebraic Combinatorics text, including:

• The first q-binomial theorem
• The second q-binomial theorem (Potter's binomial theorem)
• Counting subspaces of finite-dimensional vector spaces over finite fields
• Limits of q-binomial coefficients

Main Definitions (in namespace AlgebraicCombinatorics.QBinomialRec)

• qBinomial: The q-binomial coefficient [n choose k]_q, defined via q-Pascal recurrence
• qFactorial: The q-factorial [n]_q!
• qNat: The q-analog of natural number [n]_q

Namespace structure: All definitions in this file are in the sub-namespace AlgebraicCombinatorics.QBinomialRec to avoid conflicts with the canonical definitions in QBinomialBasic.lean. The canonical definitions use the monotone function sum formula, while this file uses the q-Pascal recurrence. Both are equivalent (see qBinomial_eq_sum_monotone).

To use definitions from this file:

• Use full path: AlgebraicCombinatorics.QBinomialRec.qBinomial
• Or open the namespace: open AlgebraicCombinatorics.QBinomialRec

Main Results

• qBinomial_eq_sum_monotone: Equivalence to the monotone function sum definition
• qBinomial_eq_sum_subsets: Equivalence to the subset sum formula
• qBinomial_first_theorem: The first q-binomial theorem
• qBinomial_second_theorem: The second q-binomial theorem (Potter's binomial theorem)
• qBinomial_subspace_count: The q-binomial coefficient counts k-dimensional subspaces
• qBinomial_limit: The limit of q-binomial coefficients as n → ∞

References

• Section on q-binomial formulas from Algebraic Combinatorics lecture notes
• See also QBinomialBasic.lean for the canonical definition and basic properties

Sub-namespace for Recursive q-Binomial Definitions

The definitions qNat, qFactorial, qBinomial, and related theorems in this file use the q-Pascal recurrence, which is different from the monotone function sum definition in QBinomialBasic.lean. To avoid namespace conflicts when both files are imported together, these definitions are placed in the QBinomialRec sub-namespace.

The equivalence between the two definitions is proven in qBinomial_eq_sum_monotone.

To use these definitions, either:

1. Open the namespace: open AlgebraicCombinatorics.QBinomialRec
2. Use the full path: AlgebraicCombinatorics.QBinomialRec.qBinomial

Definition def.pars.qbinom.qint: q-integers and q-factorials

This section formalizes the q-analogs of integers and factorials from Definition 2.3.2.

Part (a): The q-integer [n]_q = q^0 + q^1 + ... + q^{n-1} ∈ ℤ[q]

Part (b): The q-factorial [n]_q! = [1]_q · [2]_q · ... · [n]_q ∈ ℤ[q]

Part (c): For any element a of a ring A, [n]_a and [n]_a! denote the results of substituting a for q in [n]_q and [n]_q!, respectively.

Remark rmk.pars.qbinom.qint.frac

For any n ∈ ℕ:

• [n]_q = (1 - q^n)/(1 - q) (in ℤ⟦q⟧ or in the field of rational functions)
• [n]_1 = n
• [n]_1! = n!

noncomputable def AlgebraicCombinatorics.QBinomialRec.qNat {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : R

Definition def.pars.qbinom.qint (a): The q-integer [n]_q.

The q-analog of a natural number is defined as the sum: [n]_q = q^0 + q^1 + q^2 + ... + q^{n-1}

This equals (1 - q^n)/(1 - q) in appropriate rings (see qNat_eq_geom_sum). When evaluated at q = 1, this equals n (see qNat_at_one).

Equations

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

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

Definition def.pars.qbinom.qint (b): The q-factorial [n]_q!.

The q-factorial is defined as the product: [n]_q! = [1]_q · [2]_q · ... · [n]_q

When evaluated at q = 1, this equals n! (see qFactorial_at_one).

Equations

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

noncomputable def AlgebraicCombinatorics.QBinomialRec.qBinomial {R : Type u_1} [CommRing R] (q : R) : ℕ → ℕ → R

The q-binomial coefficient (Gaussian binomial coefficient) [n choose k]_q = [n]_q! / ([k]_q! · [n-k]_q!).

This is defined as a polynomial in q with integer coefficients. It counts partitions that fit in a k × (n-k) box, weighted by q^|λ|.

We use the recurrence relation (q-Pascal's identity): [n choose k]_q = [n-1 choose k-1]_q + q^k · [n-1 choose k]_q

This avoids division and works over any commutative ring.

This definition is equivalent to AlgebraicCombinatorics.qBinomial in QBinomialBasic.lean, which uses the monotone function sum definition. The equivalence is proven in qBinomial_eq_sum_monotone. The argument order here is (q : R) (n k : ℕ) vs (n k : ℕ) (q : R) in QBinomialBasic.lean.

Equations

• AlgebraicCombinatorics.QBinomialRec.qBinomial q x✝ 0 = 1
• AlgebraicCombinatorics.QBinomialRec.qBinomial q 0 n.succ = 0
• AlgebraicCombinatorics.QBinomialRec.qBinomial q n.succ k.succ = AlgebraicCombinatorics.QBinomialRec.qBinomial q n k + q ^ (k + 1) * AlgebraicCombinatorics.QBinomialRec.qBinomial q n (k + 1)

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qNat_zero {R : Type u_1} [CommRing R] (q : R) : qNat q 0 = 0

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qNat_one {R : Type u_1} [CommRing R] (q : R) : qNat q 1 = 1

theorem AlgebraicCombinatorics.QBinomialRec.qNat_succ {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qNat q (n + 1) = 1 + q * qNat q n

@[simp]

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

@[simp]

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

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

Remark rmk.pars.qbinom.qint.frac: Properties of q-integers and q-factorials

The following lemmas formalize the key properties from Remark 2.3.3:

• The geometric series formula: [n]_q = (1 - q^n)/(1 - q)
• Evaluation at 1: [n]_1 = n and [n]_1! = n!

theorem AlgebraicCombinatorics.QBinomialRec.qNat_mul_one_sub {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qNat q n * (1 - q) = 1 - q ^ n

Remark rmk.pars.qbinom.qint.frac (part 1): The q-integer equals the geometric series formula. [n]_q · (1 - q) = 1 - q^n

This is the "cleared denominator" form of [n]_q = (1 - q^n)/(1 - q). The equality holds in any commutative ring.

theorem AlgebraicCombinatorics.QBinomialRec.qNat_eq_geom_sum {F : Type u_2} [Field F] (q : F) (n : ℕ) (hq : q ≠ 1) : qNat q n = (1 - q ^ n) / (1 - q)

Remark rmk.pars.qbinom.qint.frac (part 1, field version): In a field where q ≠ 1, we have [n]_q = (1 - q^n)/(1 - q).

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qNat_at_one {R : Type u_1} [CommRing R] (n : ℕ) : qNat 1 n = ↑n

Remark rmk.pars.qbinom.qint.frac (part 2): [n]_1 = n.

When we substitute q = 1 into the q-integer, we get the ordinary integer. This follows from 1^0 + 1^1 + ... + 1^{n-1} = n.

@[simp]

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

Remark rmk.pars.qbinom.qint.frac (part 3): [n]_1! = n!.

When we substitute q = 1 into the q-factorial, we get the ordinary factorial. This follows from [1]_1 · [2]_1 · ... · [n]_1 = 1 · 2 · ... · n = n!.

@[simp]

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

The q-binomial coefficient at q = 1 equals the ordinary binomial coefficient.

This follows from the recurrence relation and the fact that [n]_1 = n.

@[simp]

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

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_gt {R : Type u_1} [CommRing R] (q : R) (n k : ℕ) (h : k > n) : qBinomial q n k = 0

Proposition prop.pars.qbinom.0: If k > n, then [n choose k]_q = 0.

This generalizes Proposition prop.binom.0 (that C(n,k) = 0 when k > n) to q-binomial coefficients.

The proof uses the partition-theoretic interpretation: [n choose k]_q is a sum over partitions with largest part ≤ n-k and length ≤ k. When k > n, we have n-k < 0, so no such partition exists, and the sum is empty (equals 0).

Alternatively, the proof proceeds by induction using the q-Pascal recurrence.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_eq_zero_of_lt {R : Type u_1} [CommRing R] (q : R) (n k : ℕ) (h : n < k) : qBinomial q n k = 0

Alias for qBinomial_gt with the hypothesis stated as n < k. This is the form used in Proposition prop.pars.qbinom.0.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_self {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qBinomial q n n = 1

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_boundary {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qBinomial q n 0 = 1 ∧ qBinomial q n n = 1

Proposition prop.pars.qbinom.n0: We have [n choose 0]_q = [n choose n]_q = 1 for each n ∈ ℕ.

This is a fundamental boundary condition for q-binomial coefficients, analogous to the classical binomial coefficient identities C(n,0) = C(n,n) = 1.

Proposition prop.pars.qbinom.alt-defs: Alternative definitions of q-binomial coefficients

This section formalizes the three equivalent characterizations of q-binomial coefficients from Proposition 11.2.4 (prop.pars.qbinom.alt-defs) of the textbook.

Part (a): Sum over weakly increasing tuples [n choose k]_q = ∑_{0 ≤ i₁ ≤ i₂ ≤ ... ≤ i_k ≤ n-k} q^{i₁ + i₂ + ... + i_k}

Part (b): Sum over k-element subsets [n choose k]_q = ∑_{S ⊆ {1,...,n}, |S| = k} q^{sum(S) - (1 + 2 + ... + k)}

Part (c): Evaluation at q = 1 gives ordinary binomial coefficient [n choose k]_1 = C(n, k)

Part (c) is already proved as qBinomial_at_one above.

def AlgebraicCombinatorics.QBinomialRec.triangular (k : ℕ) : ℕ

The triangular number T(k) = 1 + 2 + ... + k = k(k+1)/2.

Equations

• AlgebraicCombinatorics.QBinomialRec.triangular k = k * (k + 1) / 2

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.triangular_zero : triangular 0 = 0

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.triangular_one : triangular 1 = 1

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.triangular_two : triangular 2 = 3

theorem AlgebraicCombinatorics.QBinomialRec.triangular_eq_sum (k : ℕ) : triangular k = ∑ i ∈ Finset.range k, (i + 1)

The triangular number equals the sum of the first k positive integers.

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

The set of monotone (weakly increasing) functions from Fin k to Fin (m + 1). This represents k-tuples (i₁, ..., i_k) with 0 ≤ i₁ ≤ i₂ ≤ ... ≤ i_k ≤ m.

This is definitionally equal to AlgebraicCombinatorics.monotoneFunctions.

Equations

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

theorem AlgebraicCombinatorics.QBinomialRec.monotoneFunctions_eq_canonical (k m : ℕ) : monotoneFunctions k m = AlgebraicCombinatorics.monotoneFunctions k m

The local monotoneFunctions is definitionally equal to the canonical version.

def AlgebraicCombinatorics.QBinomialRec.sumValues (k m : ℕ) (f : Fin k → Fin (m + 1)) : ℕ

The sum of values of a function from Fin k to Fin (m + 1).

Equations

• AlgebraicCombinatorics.QBinomialRec.sumValues k m f = ∑ i : Fin k, ↑(f i)

def AlgebraicCombinatorics.QBinomialRec.kSubsetsOfIcc (n k : ℕ) : Finset (Finset ℕ)

The set of k-element subsets of {1, 2, ..., n}.

Equations

• AlgebraicCombinatorics.QBinomialRec.kSubsetsOfIcc n k = {S ∈ (Finset.Icc 1 n).powerset | S.card = k}

def AlgebraicCombinatorics.QBinomialRec.finsetSumNat (S : Finset ℕ) : ℕ

The sum of elements in a finite set of natural numbers.

Note: This is named finsetSumNat to distinguish from AlgebraicCombinatorics.CauchyBinet.finsetSumFin, which computes the sum of elements in a Finset (Fin n) by extracting their .val. Both compute "the sum of elements" but for different element types.

Equations

• AlgebraicCombinatorics.QBinomialRec.finsetSumNat S = S.sum id

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_eq_sum_monotone {R : Type u_1} [CommRing R] (q : R) (n k : ℕ) (hk : k ≤ n) : qBinomial q n k = ∑ f ∈ monotoneFunctions k (n - k), q ^ sumValues k (n - k) f

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_eq_sum_subsets {R : Type u_1} [CommRing R] (q : R) (n k : ℕ) : qBinomial q n k = ∑ S ∈ kSubsetsOfIcc n k, q ^ (finsetSumNat S - triangular k)

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_eq_prod_div {F : Type u_2} [Field F] (q : F) (n k : ℕ) (hk : k ≤ n) (hq : ∀ i < k, qNat q (i + 1) ≠ 0) : qBinomial q n k = ∏ i ∈ Finset.range k, qNat q (n - i) / qNat q (i + 1)

The q-binomial coefficient satisfies the product formula over a field: [n choose k]q = ∏{i=0}^{k-1} [n-i]_q / [i+1]_q

This is equivalent to the recursive definition when q is not a root of unity.

Combinatorial Definition of q-Binomial Coefficients (Definition def.pars.qbinom.qbinom)

This section formalizes Definition 4.3.2 from the textbook, which defines the q-binomial coefficient (Gaussian binomial coefficient) as a sum over partitions:

(a) The q-binomial coefficient [n choose k]_q is the polynomial ∑_{λ} q^|λ| where λ ranges over all partitions with largest part ≤ n-k and length ≤ k.

(b) For any ring element a, the evaluation [n choose k]_a is obtained by substituting a for q in the polynomial [n choose k]_q.

Key Properties

• When k > n, the q-binomial is 0 (empty sum since n - k < 0).
• [n choose 0]_q = [n choose n]_q = 1 (only the empty partition qualifies).
• When a = 1, we recover the ordinary binomial coefficient: [n choose k]_1 = C(n,k).

def AlgebraicCombinatorics.QBinomialRec.partitionLargestPartLeq {n : ℕ} (p : n.Partition) (m : ℕ) : Prop

A partition has largest part ≤ m if all parts are ≤ m. This is used in the combinatorial definition of q-binomial coefficients.

Equations

• AlgebraicCombinatorics.QBinomialRec.partitionLargestPartLeq p m = ∀ i ∈ p.parts, i ≤ m

def AlgebraicCombinatorics.QBinomialRec.partitionLengthLeq {n : ℕ} (p : n.Partition) (k : ℕ) : Prop

A partition has length ≤ k if it has at most k parts. This is used in the combinatorial definition of q-binomial coefficients.

Equations

• AlgebraicCombinatorics.QBinomialRec.partitionLengthLeq p k = (p.parts.card ≤ k)

instance AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionLargestPartLeq {n m : ℕ} (p : n.Partition) : Decidable (partitionLargestPartLeq p m)

Equations

• AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionLargestPartLeq p = inferInstanceAs (Decidable (∀ i ∈ p.parts, i ≤ m))

instance AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionLengthLeq {n k : ℕ} (p : n.Partition) : Decidable (partitionLengthLeq p k)

Equations

• AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionLengthLeq p = inferInstanceAs (Decidable (p.parts.card ≤ k))

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

The set of partitions of a given size that fit in a k × m box (i.e., have length ≤ k and largest part ≤ m).

For the q-binomial [n choose k]_q, we use m = n - k.

Argument order: (size k m : ℕ) where:

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

This matches the convention in AlgebraicCombinatorics.partitionsInBox from QBinomialBasic.lean.

Equations

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

def AlgebraicCombinatorics.QBinomialRec.countPartitionsInBox (size k m : ℕ) : ℕ

The count of partitions of a given size that fit in a k × m box.

Equations

• AlgebraicCombinatorics.QBinomialRec.countPartitionsInBox size k m = (AlgebraicCombinatorics.QBinomialRec.partitionsInBox size k m).card

def AlgebraicCombinatorics.QBinomialRec.partitionsInBoxExact (size k m : ℕ) : Finset size.Partition

Partitions with exactly k parts (not just at most k parts), fitting in a box with largest part ≤ m. Used in the q-Pascal identity proof to split partitions by exact number of parts.

Equations

• AlgebraicCombinatorics.QBinomialRec.partitionsInBoxExact size k m = {p : size.Partition | p.parts.card = k ∧ AlgebraicCombinatorics.QBinomialRec.partitionLargestPartLeq p m}

instance AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionsInBoxExact {size k m : ℕ} (p : size.Partition) : Decidable (p.parts.card = k ∧ partitionLargestPartLeq p m)

Equations

• AlgebraicCombinatorics.QBinomialRec.instDecidablePartitionsInBoxExact p = inferInstanceAs (Decidable (p.parts.card = k ∧ ∀ i ∈ p.parts, i ≤ m))

theorem AlgebraicCombinatorics.QBinomialRec.partitionsInBoxExact_card_eq (s k m : ℕ) (hm : m ≥ 1) (hs : s ≥ k + 1) : (partitionsInBoxExact s (k + 1) m).card = countPartitionsInBox (s - (k + 1)) (k + 1) (m - 1)

Key cardinality equality: partitions with exactly k+1 parts in (k+1) × m box biject with partitions with at most k+1 parts in (k+1) × (m-1) box, via the "subtract 1 from each part" bijection. This is the combinatorial heart of the q-Pascal identity.

The bijection:

• Forward: subtract 1 from each part, filter zeros (using ofSums)
• Inverse: add 1 to each part, pad with 1s to get exactly k+1 parts

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

The q-binomial coefficient as a polynomial in ℤ[q]. (Definition def.pars.qbinom.qbinom (a))

[n choose k]_q = ∑_{λ} q^|λ|

where λ ranges over all partitions with largest part ≤ n-k and length ≤ k.

This is a polynomial (not just a formal power series) because there are finitely many such partitions - they all fit in a k × (n-k) box, so their size is at most k · (n-k).

When k > n, this is 0 (the empty sum, since n - k < 0 means no partitions qualify).

Equations

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

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialPolyDef_of_gt (n k : ℕ) (h : k > n) : qBinomialPolyDef n k = 0

When k > n, the combinatorial q-binomial coefficient is 0.

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialPolyDef_zero_right (n : ℕ) : qBinomialPolyDef n 0 = 1

[n choose 0]_q = 1 for all n.

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialPolyDef_self (n : ℕ) : qBinomialPolyDef n n = 1

[n choose n]_q = 1 for all n.

noncomputable def AlgebraicCombinatorics.QBinomialRec.qBinomialEval {R : Type u_1} [CommRing R] (n k : ℕ) (a : R) : R

The q-binomial coefficient evaluated at a ring element. (Definition def.pars.qbinom.qbinom (b))

[n choose k]_a = ∑_{λ} a^|λ|

where λ ranges over all partitions with largest part ≤ n-k and length ≤ k.

This is the result of substituting a for q in the polynomial [n choose k]_q.

Equations

• AlgebraicCombinatorics.QBinomialRec.qBinomialEval n k a = Polynomial.eval₂ (Int.castRingHom R) a (AlgebraicCombinatorics.QBinomialRec.qBinomialPolyDef n k)

def AlgebraicCombinatorics.QBinomialRec.qBinomialEvalDirect {R : Type u_1} [CommRing R] (n k : ℕ) (a : R) : R

Alternative definition: directly sum over partitions.

Equations

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

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialEval_eq_direct {R : Type u_1} [CommRing R] (n k : ℕ) (a : R) : qBinomialEval n k a = qBinomialEvalDirect n k a

The two definitions of qBinomialEval agree.

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialEval_of_gt {R : Type u_1} [CommRing R] (n k : ℕ) (h : k > n) (a : R) : qBinomialEval n k a = 0

When k > n, the evaluated q-binomial is 0.

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialEval_zero_right {R : Type u_1} [CommRing R] (n : ℕ) (a : R) : qBinomialEval n 0 a = 1

[n choose 0]_a = 1 for all n and a.

@[simp]

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialEval_self {R : Type u_1} [CommRing R] (n : ℕ) (a : R) : qBinomialEval n n a = 1

[n choose n]_a = 1 for all n and a.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialPolyDef_pascal (n k : ℕ) (hk : k + 1 ≤ n + 1) : qBinomialPolyDef (n + 1) (k + 1) = qBinomialPolyDef n k + Polynomial.X ^ (k + 1) * qBinomialPolyDef n (k + 1)

The q-Pascal identity for qBinomialPolyDef (polynomial version). This is the combinatorial heart of the proof connecting the two definitions.

The identity states: [n+1 choose k+1]_q = [n choose k]_q + q^{k+1} · [n choose k+1]_q

Combinatorially, partitions in a (k+1) × (n-k) box split into two types:

1. Those with length ≤ k (same as partitions in k × (n-k) box)
2. Those with length = k+1, which biject with partitions in (k+1) × (n-k-1) box via "removing a column" (subtracting 1 from each of the k+1 parts), with size decreased by k+1 (hence the factor q^{k+1}).

theorem AlgebraicCombinatorics.QBinomialRec.qBinomialEval_eq_qBinomial {R : Type u_1} [CommRing R] (n k : ℕ) (q : R) : qBinomialEval n k q = qBinomial q n k

The combinatorial definition agrees with the recursive definition. This connects Definition def.pars.qbinom.qbinom with the recurrence-based qBinomial.

The proof shows that both definitions satisfy the same recurrence relation (q-Pascal's identity) and boundary conditions.

theorem AlgebraicCombinatorics.QBinomialRec.prod_add_eq_sum_over_subsets {L : Type u_1} [CommRing L] {n : ℕ} (a b : Fin n → L) : ∏ i : Fin n, (a i + b i) = ∑ S : Finset (Fin n), (∏ i ∈ S, a i) * ∏ i ∈ Sᶜ, b i

Lemma lem.prodrule.sum-ai-plus-bi: Product expansion rule. When expanding ∏ᵢ (aᵢ + bᵢ), we get a sum over all subsets S of [n], where each term is (∏{i ∈ S} aᵢ) · (∏{i ∉ S} bᵢ).

This is a fundamental identity used in proofs of the q-binomial theorems and determinant formulas.

A rigorous proof can be found in [detnotes, Exercise 6.1 (a)].

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_induction_identity {K : Type u_1} [CommRing K] (q : K) (n k : ℕ) : q ^ k * qBinomial q n (k + 1) + q ^ n * qBinomial q n k = q ^ k * qBinomial q n k + q ^ (k + 1) * q ^ k * qBinomial q n (k + 1)

Key algebraic identity for the induction step of qBinomial_sum_subsets.

This identity holds because qBinomial satisfies specific algebraic relations. The proof uses induction on n, showing that the identity follows from the recurrence relation for qBinomial.

Specifically, we need: q^k * qBinomial q n (k+1) + q^n * qBinomial q n k = q^k * qBinomial q n k + q^(2k+1) * qBinomial q n (k+1)

This is equivalent to: (q^n - q^k) * qBinomial q n k = q^k * (q^(k+1) - 1) * qBinomial q n (k+1)

The proof proceeds by induction on n, using the specific structure of qBinomial coefficients. The identity follows from the fact that qBinomial can be expressed as a geometric sum.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_sum_subsets {K : Type u_1} [CommRing K] (q : K) (n k : ℕ) : ∑ S ∈ (Finset.range n).powerset with S.card = k, q ^ ∑ i ∈ S, i = q ^ (k * (k - 1) / 2) * qBinomial q n k

Key lemma: The sum over k-element subsets of {0, 1, ..., n-1} of q^{sum(S)} equals q^{k(k-1)/2} * [n choose k]_q.

This is the combinatorial interpretation of q-binomial coefficients from Proposition prop.pars.qbinom.alt-defs part (b) in the textbook.

The formula arises because:

• [n choose k]_q counts k-element subsets weighted by q^{sum(S) - (1+2+...+k)}
• In 0-indexed form, this becomes q^{sum(S)} = q^{k(k-1)/2} * [n choose k]_q

The proof proceeds by induction on n, using the q-Pascal recurrence.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_first_theorem {K : Type u_1} [CommRing K] (a b q : K) (n : ℕ) : ∏ i ∈ Finset.range n, (a * q ^ i + b) = ∑ k ∈ Finset.range (n + 1), q ^ (k * (k - 1) / 2) * qBinomial q n k * a ^ k * b ^ (n - k)

Theorem thm.pars.qbinom.binom1: First q-binomial theorem. For a, b ∈ K and n ∈ ℕ, in the polynomial ring K[q], we have: (aq⁰ + b)(aq¹ + b)···(aqⁿ⁻¹ + b) = ∑_{k=0}^{n} q^{k(k-1)/2} · [n choose k]_q · aᵏ · bⁿ⁻ᵏ

Setting q = 1 recovers the classical binomial formula (a + b)ⁿ.

The proof uses the product expansion lemma (lem.prodrule.sum-ai-plus-bi):

• Expand the product as a sum over subsets S ⊆ {0, 1, ..., n-1}
• For each S, the contribution is a^|S| * q^{∑_{i ∈ S} i} * b^{n - |S|}
• Group by cardinality k = |S|
• Use qBinomial_sum_subsets to evaluate the sum over k-element subsets

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_first_theorem_at_one {K : Type u_1} [CommRing K] (a b : K) (n : ℕ) : ∏ _i ∈ Finset.range n, (a + b) = ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * a ^ k * b ^ (n - k)

The first q-binomial theorem specializes to the binomial formula when q = 1.

theorem AlgebraicCombinatorics.QBinomialRec.b_mul_pow_a {L : Type u_1} [CommRing L] {A : Type u_2} [Ring A] [Algebra L A] (ω : L) (a b : A) (hab : b * a = ω • (a * b)) (k : ℕ) : b * a ^ k = ω ^ k • (a ^ k * b)

Helper lemma: b * a^k = ω^k * a^k * b for the twisted commutativity relation.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_second_theorem {L : Type u_1} [CommRing L] {A : Type u_2} [Ring A] [Algebra L A] (ω : L) (a b : A) (hab : b * a = ω • (a * b)) (n : ℕ) : (a + b) ^ n = ∑ k ∈ Finset.range (n + 1), qBinomial ω n k • (a ^ k * b ^ (n - k))

Theorem thm.pars.qbinom.binom2: Second q-binomial theorem (Potter's binomial theorem). Let A be a noncommutative L-algebra, and let a, b ∈ A satisfy ba = ω·ab for some ω ∈ L. Then (a + b)ⁿ = ∑_{k=0}^{n} [n choose k]_ω · aᵏ · bⁿ⁻ᵏ.

This generalizes the binomial formula to the noncommutative setting with a "twisted" commutativity relation.

theorem AlgebraicCombinatorics.QBinomialRec.linearIndependent_iff_not_mem_span_of_lt {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] {k : ℕ} (v : Fin k → V) : LinearIndependent F v ↔ ∀ (i : Fin k), v i ∉ Submodule.span F (v '' {j : Fin k | ↑j < ↑i})

Lemma lem.linalg.lin-ind-via-span: A k-tuple (v₁, v₂, ..., vₖ) is linearly independent if and only if each vᵢ ∉ span{v₁, ..., vᵢ₋₁}.

This is the inductive characterization of linear independence.

theorem AlgebraicCombinatorics.QBinomialRec.card_linearIndependent_tuples {F : Type u_1} [Field F] [Fintype F] {V : Type u_2} [AddCommGroup V] [Module F V] [Module.Finite F V] (n k : ℕ) (hn : Module.finrank F V = n) : Nat.card { v : Fin k → V // LinearIndependent F v } = ∏ i ∈ Finset.range k, (Fintype.card F ^ n - Fintype.card F ^ i)

Lemma lem.pars.qbinom.lin-ind-count: The number of linearly independent k-tuples of vectors in an n-dimensional F-vector space V is ∏_{i=0}^{k-1} (|F|ⁿ - |F|ⁱ).

The proof proceeds by induction on k:

• Base case (k = 0): There is exactly one 0-tuple, which is vacuously linearly independent.
• Inductive step: A linearly independent (k+1)-tuple (v₁, ..., v_{k+1}) corresponds to a linearly independent k-tuple (v₂, ..., v_{k+1}) together with a choice of v₁ outside the span of {v₂, ..., v_{k+1}}. The span has |F|^k elements, so there are |F|^n - |F|^k choices for v₁.

This uses card_linearIndependent from Mathlib which proves this via the equivalence equiv_linearIndependent.

theorem AlgebraicCombinatorics.QBinomialRec.card_eq_mul_of_fibers {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] [DecidableEq B] (f : A → B) (m : ℕ) (hf : ∀ (b : B), Fintype.card { a : A // f a = b } = m) : Fintype.card A = m * Fintype.card B

Lemma lem.count.multijection: Multijection principle. If f : A → B is a map such that each b ∈ B has exactly m preimages, then |A| = m · |B|.

This is a fundamental counting principle used throughout combinatorics. A map f satisfying this assumption is called an m-to-1 map.

The proof uses the fiber decomposition: |A| = Σ_{b ∈ B} |fiber(b)|, where each fiber has cardinality m by assumption.

noncomputable def AlgebraicCombinatorics.QBinomialRec.spanMap {F : Type u_1} [Field F] {V : Type u_2} [AddCommGroup V] [Module F V] (k : ℕ) : { v : Fin k → V // LinearIndependent F v } → { W : Submodule F V // Module.finrank F ↥W = k }

The span map sends a linearly independent k-tuple to its span (a k-dimensional subspace).

Equations

• AlgebraicCombinatorics.QBinomialRec.spanMap k ⟨v, hv⟩ = ⟨Submodule.span F (Set.range v), ⋯⟩

theorem AlgebraicCombinatorics.QBinomialRec.spanMap_fiber_card {F : Type u_1} [Field F] [Fintype F] {V : Type u_2} [AddCommGroup V] [Module F V] [Module.Finite F V] (k : ℕ) (W : { W : Submodule F V // Module.finrank F ↥W = k }) : Nat.card { v : { v : Fin k → V // LinearIndependent F v } // spanMap k v = W } = ∏ i ∈ Finset.range k, (Fintype.card F ^ k - Fintype.card F ^ i)

Key lemma for thm.pars.qbinom.subsp-count: Each k-dimensional subspace W has exactly ∏_{i=0}^{k-1} (q^k - q^i) preimages under the span map.

This is because the preimages are exactly the ordered bases of W:

• A linearly independent k-tuple v with span(v) = W must lie entirely in W
• Since W is k-dimensional and v has k linearly independent vectors, v spans W automatically
• Thus the preimages are exactly the linearly independent k-tuples in W
• By card_linearIndependent, the count is ∏_{i=0}^{k-1} (q^k - q^i)

This is the key step in the proof of qBinomial_subspace_count.

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_subspace_count {F : Type u_1} [Field F] [Fintype F] {V : Type u_2} [AddCommGroup V] [Module F V] [Module.Finite F V] (n k : ℕ) (hn : Module.finrank F V = n) : qBinomial (↑(Fintype.card F)) n k = ↑(Nat.card { W : Submodule F V // Module.finrank F ↥W = k })

Theorem thm.pars.qbinom.subsp-count: The q-binomial coefficient at |F| counts k-dimensional subspaces. If V is an n-dimensional vector space over a finite field F, then [n choose k]_{|F|} = (# of k-dimensional subspaces of V).

This is the "linear analogue" of the fact that C(n,k) counts k-element subsets of an n-element set.

Proof outline

The proof uses the multijection principle (Lemma lem.count.multijection):

1. Define the span map f : (linearly independent k-tuples in V) → (k-dim subspaces of V) that sends a tuple v to its span span(v).

2. By card_linearIndependent_tuples: |linearly independent k-tuples in V| = ∏_{i=0}^{k-1} (q^n - q^i)

3. By spanMap_fiber_card, each k-dimensional subspace W has exactly ∏_{i=0}^{k-1} (q^k - q^i) preimages under f (the number of ordered bases of W).

4. By the multijection principle: ∏{i=0}^{k-1} (q^n - q^i) = (∏{i=0}^{k-1} (q^k - q^i)) × (# of k-dim subspaces)

5. Therefore: (# of k-dim subspaces) = ∏{i=0}^{k-1} (q^n - q^i) / ∏{i=0}^{k-1} (q^k - q^i) = [n choose k]_q

noncomputable def AlgebraicCombinatorics.QBinomialRec.partitionCountAtMostKParts (n k : ℕ) : ℕ

The number of partitions of n with at most k parts.

Equations

• AlgebraicCombinatorics.QBinomialRec.partitionCountAtMostKParts n k = Nat.card { p : n.Partition // p.parts.card ≤ k }

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_coeff_eq (d k n m : ℕ) (hn : n ≥ d + k) (hm : m ≥ d + k) : (PowerSeries.coeff d) (qBinomial PowerSeries.X n k) = (PowerSeries.coeff d) (qBinomial PowerSeries.X m k)

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_stable_eq_prod (d k : ℕ) : (PowerSeries.coeff d) (qBinomial PowerSeries.X (d + k) k) = (PowerSeries.coeff d) (∏ i ∈ Finset.range k, (1 - PowerSeries.X ^ (i + 1))⁻¹)

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_limit (k : ℕ) : Filter.Tendsto (fun (n : ℕ) => qBinomial PowerSeries.X n k) Filter.atTop (nhds (∏ i ∈ Finset.range k, (1 - PowerSeries.X ^ (i + 1))⁻¹))

Proposition prop.pars.qbinom.lim1: Limit of q-binomial coefficients. As n → ∞, the q-binomial coefficient [n choose k]q converges coefficientwise to ∑{n ∈ ℕ} (p₀(n) + p₁(n) + ... + pₖ(n)) qⁿ = ∏_{i=1}^{k} 1/(1 - qⁱ)

where pᵢ(n) is the number of partitions of n with exactly i parts.

This is stated for power series over a field where inverses exist.

theorem AlgebraicCombinatorics.QBinomialRec.conjugatePartition_involution' (m : ℕ) (p : m.Partition) : AlgebraicCombinatorics.QBinomialRec.conjugatePartition'✝ m (AlgebraicCombinatorics.QBinomialRec.conjugatePartition'✝¹ m p) = p

theorem AlgebraicCombinatorics.QBinomialRec.restricted_card_eq_atMostKParts (n k : ℕ) : (Nat.Partition.restricted n fun (x : ℕ) => x ≤ k).card = partitionCountAtMostKParts n k

theorem AlgebraicCombinatorics.QBinomialRec.qBinomial_limit_eq_partition_gf (k : ℕ) : ∏ i ∈ Finset.range k, (1 - PowerSeries.X ^ (i + 1))⁻¹ = PowerSeries.mk fun (n : ℕ) => ↑(partitionCountAtMostKParts n k)

The limit of q-binomial coefficients equals the generating function for partitions with at most k parts.

This is the second equality in Proposition prop.pars.qbinom.lim1: ∑{n ∈ ℕ} (p₀(n) + p₁(n) + ... + pₖ(n)) qⁿ = ∏{i=1}^{k} 1/(1 - qⁱ)

Combined with Theorem thm.pars.main-gf-0n from the partition generating functions section.