Gaussian binomial coefficients

DefinitionGaussian binomial coefficient#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For natural numbers \(M\) and \(k\), the Gaussian binomial coefficient \(\binom{M}{k}_Q \in R\) is defined recursively by \(\binom{M}{0}_Q = 1\), \(\binom{0}{k+1}_Q = 0\) and \(\binom{M+1}{k+1}_Q = \binom{M}{k}_Q + Q^{k+1} \binom{M}{k+1}_Q\).

def gaussBinom {R : Type*} [Semiring R] (Q : R) (M : ℕ) : ℕ → R
  | 0 => 1
  | k + 1 =>
      match M with
      | 0 => 0
      | M + 1 => gaussBinom Q M k + Q ^ (k + 1) * gaussBinom Q M (k + 1)

Used by 21

Used byRogers–Ramanujan identity (first form) · Generating function for fixed column hooks of size \(k\) in distinct partitions · Generating function for fixed column hooks of size \(k\) · Fixed column hooks of size \(k\) in odd distinct partitions, even column · Generating function for fixed column hooks of size \(k\) in odd partitions · Fixed column hooks from a part of size \(k\) in distinct partitions · Generating function for fixed column hooks from a part of size \(k\) · Odd partitions with a fixed hook in a given column arising from an odd part · Partitions with a fixed first-column hook of given size · Partitions with a fixed first-column hook arising from a part of given size · Lit cells of weakly decreasing partitions with few parts · Triangular \(q\)-binomial coefficients via Gaussian binomials · Gaussian binomial coefficients vanish when \(k > M\) · Product formula for Gaussian binomial coefficients · Diagonal Gaussian binomial coefficients · \(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(k = 0\) · Gaussian binomial coefficients with \(M = 0\) · The \((p, q)\)-binomial coefficients at \(p = 1\) · Jacobi's cube identity · Jacobi triple product identity

TheoremGaussian binomial coefficients with \(k = 0\)#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For every natural number \(M\), the Gaussian binomial coefficient \(\binom{M}{0}_Q\) equals \(1\).

@[simp]
theorem gaussBinom_zero_right {R : Type*} [Semiring R] (Q : R) (M : ℕ) :
    gaussBinom Q M 0 = 1

Uses 1 · Used by 6

Statement usesGaussian binomial coefficient

Used byRogers–Ramanujan identity (first form) · Product formula for Gaussian binomial coefficients · Diagonal Gaussian binomial coefficients · The \((p, q)\)-binomial coefficients at \(p = 1\) · Jacobi's cube identity · Jacobi triple product identity

TheoremGaussian binomial coefficients with \(M = 0\)#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For every natural number \(k\), the Gaussian binomial coefficient \(\binom{0}{k+1}_Q\) equals \(0\).

@[simp]
theorem gaussBinom_zero_succ {R : Type*} [Semiring R] (Q : R) (k : ℕ) :
    gaussBinom Q 0 (k + 1) = 0

Uses 1 · Used by 3

Statement usesGaussian binomial coefficient

Used byGaussian binomial coefficients vanish when \(k > M\) · The \((p, q)\)-binomial coefficients at \(p = 1\) · Jacobi's cube identity

Theorem\(Q\)-Pascal recursion for Gaussian binomial coefficients#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For all natural numbers \(M\) and \(k\), the Gaussian binomial coefficients satisfy \(\binom{M+1}{k+1}_Q = \binom{M}{k}_Q + Q^{k+1} \binom{M}{k+1}_Q\).

theorem gaussBinom_succ_succ {R : Type*} [Semiring R] (Q : R)
    (M k : ℕ) :
    gaussBinom Q (M + 1) (k + 1)
      = gaussBinom Q M k + Q ^ (k + 1) * gaussBinom Q M (k + 1)

Uses 1 · Used by 7

Statement usesGaussian binomial coefficient

Used byRogers–Ramanujan identity (first form) · Gaussian binomial coefficients vanish when \(k > M\) · Product formula for Gaussian binomial coefficients · Diagonal Gaussian binomial coefficients · The \((p, q)\)-binomial coefficients at \(p = 1\) · Jacobi's cube identity · Jacobi triple product identity

TheoremGaussian binomial coefficients vanish when \(k > M\)#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For natural numbers \(M\) and \(k\) with \(M < k\), the Gaussian binomial coefficient \(\binom{M}{k}_Q\) is \(0\).

theorem gaussBinom_eq_zero_of_lt {R : Type*} [Semiring R] (Q : R)
    (M k : ℕ) (h : M < k) : gaussBinom Q M k = 0

Uses 3 · Used by 4

Statement usesGaussian binomial coefficient

Proof uses\(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(M = 0\)

Used byRogers–Ramanujan identity (first form) · Diagonal Gaussian binomial coefficients · Jacobi's cube identity · Jacobi triple product identity

TheoremDiagonal Gaussian binomial coefficients#✓fully proved

Let \(R\) be a semiring and \(Q \in R\). For every natural number \(M\), the Gaussian binomial coefficient \(\binom{M}{M}_Q\) equals \(1\).

@[simp]
theorem gaussBinom_self {R : Type*} [Semiring R] (Q : R) (M : ℕ) :
    gaussBinom Q M M = 1

Uses 4 · Used by 4

Statement usesGaussian binomial coefficient

Proof usesGaussian binomial coefficients vanish when \(k > M\) · \(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(k = 0\)

Used byRogers–Ramanujan identity (first form) · Product formula for Gaussian binomial coefficients · The \((p, q)\)-binomial coefficients at \(p = 1\) · Jacobi's cube identity

DefinitionFinite \(Q\)-Pochhammer symbol#✓fully proved

Let \(R\) be a commutative ring and \(Q \in R\). For a natural number \(m\), the finite \(Q\)-Pochhammer symbol \(P_Q(m) \in R\) is the product \(\prod_{i < m} (1 - Q^{i+1})\) of \(1 - Q^{i+1}\) over the natural numbers \(i < m\).

def qPochFin {R : Type*} [CommRing R] (Q : R) (m : ℕ) : R :=
  ∏ i ∈ Finset.range m, (1 - Q ^ (i + 1))

Used by 17

Used byRogers–Ramanujan identity (first form) · Generating function for column-\(m\) hooks of size \(k\) · Limit of the fixed-hook generating functions · Generating function for fixed column hooks of size \(k\) in distinct partitions · Generating function for fixed column hooks of size \(k\) · Fixed column hooks of size \(k\) in odd distinct partitions, even column · Generating function for fixed column hooks of size \(k\) in odd partitions · Fixed column hooks from a part of size \(k\) in distinct partitions · Generating function for fixed column hooks from a part of size \(k\) · Odd partitions with a fixed hook in a given column arising from an odd part · Partitions with a fixed first-column hook of given size · Partitions with a fixed first-column hook arising from a part of given size · Product formula for Gaussian binomial coefficients · Recursion for the finite \(Q\)-Pochhammer symbol · The finite \(Q\)-Pochhammer symbol at \(0\) · Jacobi's cube identity · Jacobi triple product identity

TheoremThe finite \(Q\)-Pochhammer symbol at \(0\)#✓fully proved

Let \(R\) be a commutative ring and \(Q \in R\). The finite \(Q\)-Pochhammer symbol \(P_Q(m) = \prod_{i < m} (1 - Q^{i+1})\), the product running over the natural numbers \(i < m\), satisfies \(P_Q(0) = 1\).

@[simp]
theorem qPochFin_zero {R : Type*} [CommRing R] (Q : R) :
    qPochFin Q 0 = 1

Uses 1 · Used by 1

Statement usesFinite \(Q\)-Pochhammer symbol

Used byProduct formula for Gaussian binomial coefficients

TheoremRecursion for the finite \(Q\)-Pochhammer symbol#✓fully proved

Let \(R\) be a commutative ring and \(Q \in R\), and write \(P_Q(m) = \prod_{i < m} (1 - Q^{i+1})\) for the finite \(Q\)-Pochhammer symbol, the product running over the natural numbers \(i < m\). For every natural number \(m\), \(P_Q(m+1) = P_Q(m) \, (1 - Q^{m+1})\).

theorem qPochFin_succ {R : Type*} [CommRing R] (Q : R) (m : ℕ) :
    qPochFin Q (m + 1) = qPochFin Q m * (1 - Q ^ (m + 1))

Uses 1 · Used by 2

Statement usesFinite \(Q\)-Pochhammer symbol

Used byProduct formula for Gaussian binomial coefficients · Jacobi's cube identity

TheoremProduct formula for Gaussian binomial coefficients#✓fully proved

Let \(R\) be a commutative ring and \(Q \in R\), and write \(P_Q(m) = \prod_{i < m} (1 - Q^{i+1})\) for the finite \(Q\)-Pochhammer symbol, the product running over the natural numbers \(i < m\). For natural numbers \(k \le M\), the Gaussian binomial coefficient satisfies \(\binom{M}{k}_Q \, P_Q(k) \, P_Q(M - k) = P_Q(M)\).

theorem gaussBinom_mul_qPochFin_mul_qPochFin {R : Type*}
    [CommRing R] (Q : R) (M k : ℕ) (h : k ≤ M) :
    gaussBinom Q M k * qPochFin Q k * qPochFin Q (M - k)
      = qPochFin Q M

Uses 7 · Used by 3

Statement usesGaussian binomial coefficient · Finite \(Q\)-Pochhammer symbol

Proof usesDiagonal Gaussian binomial coefficients · \(Q\)-Pascal recursion for Gaussian binomial coefficients · Gaussian binomial coefficients with \(k = 0\) · Recursion for the finite \(Q\)-Pochhammer symbol · The finite \(Q\)-Pochhammer symbol at \(0\)

Used byRogers–Ramanujan identity (first form) · Jacobi's cube identity · Jacobi triple product identity

TheoremEhrenborg–Readdy expansion of the Gaussian coefficient#✓fully proved

Let \(n\) and \(k\) be natural numbers and let \(W\) be the set of words \(v = v_0 v_1 \cdots v_{n-1}\) over the alphabet \(\{0, 1\}\) with exactly \(k\) letters equal to \(1\). For a word \(v\), let \(\operatorname{inv}(v)\) be the number of pairs \(i < j\) with \(v_i > v_j\); call \(v\) pair-sorted when \(v_{2i} \le v_{2i+1}\) for every \(i\) with \(2i + 1 < n\); and let \(\operatorname{asc}_{\mathrm{odd}}(v)\) be the number of \(i\) with \(2i + 1 < n\) and \(v_{2i} < v_{2i+1}\). Then, in the polynomial ring \(\mathbb{N}[q]\),

\[\sum_{v \in W} q^{\operatorname{inv}(v)} = \sum_{v \in W,\ v \text{ pair-sorted}} q^{\operatorname{inv}(v)} (1 + q)^{\operatorname{asc}_{\mathrm{odd}}(v)}.\]

The left side is MacMahon's inversion generating polynomial of \(W\), which equals the Gaussian coefficient \(\binom{n}{k}_q\). Positions are numbered from \(0\), so the pairs \((v_{2i}, v_{2i+1})\) are the source's pairs of positions \((1, 2), (3, 4), \ldots\), and \(\operatorname{asc}_{\mathrm{odd}}\) counts its odd ascents.

MetaMathlibExt.gaussian_pair_sorted_expansion · 18 lines

theorem gaussian_pair_sorted_expansion (n k : ℕ) :
  let words : Finset (Fin n → Fin 2) :=
    Finset.univ.filter
      (fun v => (Finset.univ.filter (fun i : Fin n => v i = (1 : Fin 2))).card = k);
  let inv : (Fin n → Fin 2) → ℕ :=
    fun v => (Finset.univ.filter
      (fun p : Fin n × Fin n => p.1 < p.2 ∧ v p.1 > v p.2)).card;
  let pairSorted : (Fin n → Fin 2) → Bool :=
    fun v => decide (∀ j j' : Fin n, j.val % 2 = 0 →
      j'.val = j.val + 1 → v j ≤ v j');
  let ascOdd : (Fin n → Fin 2) → ℕ :=
    fun v => (Finset.univ.filter
      (fun j : Fin n => j.val % 2 = 0 ∧
        ∃ j' : Fin n, j'.val = j.val + 1 ∧ v j < v j')).card;
  Finset.sum words (fun v => (Polynomial.X : Polynomial ℕ) ^ inv v) =
    Finset.sum (words.filter (fun v => pairSorted v = true))
      (fun v => (Polynomial.X : Polynomial ℕ) ^ inv v *
        ((1 : Polynomial ℕ) + Polynomial.X) ^ ascOdd v)

Sources

• Richard Ehrenborg and Margaret A. Readdy, "The Gaussian Coefficient Revisited," Journal of Integer Sequences 19 (2016), Article 16.7.8, Corollary 3, equation, lines 301–311, https://cs.uwaterloo.ca/journals/JIS/VOL19/Ehrenborg/ehr3.tex

11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.