q-Pochhammer symbol and Gaussian binomial coefficient

This file defines the finite q-Pochhammer symbol $(a;q)_n$ and the Gaussian binomial coefficient $\binom{n}{k}_q$, together with their basic properties.

Main definitions

• QSeries.qPochhammer a q n — the finite q-Pochhammer symbol $(a;q)_n = \prod_{k=0}^{n-1}(1 - a q^k)$.
• QSeries.qBinom n k q — the Gaussian binomial coefficient $\binom{n}{k}_q$, defined via the q-Pascal recurrence.

Main results

• QSeries.qPochhammer_succ — the recurrence $(a;q)_{n+1} = (a;q)_n (1 - aq^n)$.
• QSeries.qBinom_succ_succ — the q-Pascal recurrence.
• QSeries.qBinom_eq_zero_of_lt — vanishing above the diagonal.
• QSeries.qBinom_self — diagonal value is 1.
• QSeries.qBinom_mul_qPochhammer_mul_qPochhammer — closed-form identity $\binom{n}{k}_q (q;q)_k (q;q)_{n-k} = (q;q)_n$.

theorem QSeries.Nat.choose_two_succ (n : ℕ) : (n + 1).choose 2 = n.choose 2 + n

Pascal's rule specialised to C(·, 2).

theorem QSeries.Nat.choose_two_add_choose_two (m k : ℕ) : (m + k).choose 2 + m.choose 2 + m = k.choose 2 + m * (m + k)

C(m+k,2) + C(m,2) + m = C(k,2) + m*(m+k).

theorem QSeries.Nat.choose_two_add_choose_two' (n l : ℕ) : n.choose 2 + (n + (l + 1)).choose 2 + (n + (l + 1)) = (l + 2).choose 2 + n * (n + (l + 1))

C(n,2) + C(n+l+1,2) + (n+l+1) = C(l+2,2) + n*(n+l+1).

theorem QSeries.Nat.le_choose_two_add_one (k : ℕ) : k ≤ k.choose 2 + 1

C(k,2) is at least k - 1.

theorem QSeries.Nat.lt_choose_two_of_add_two_le {d k : ℕ} (hk : d + 2 ≤ k) : d < k.choose 2

C(k,2) eventually dominates: d < C(k,2) as soon as d + 2 ≤ k.

def QSeries.qPochhammer {R : Type u_1} [CommRing R] (a q : R) (n : ℕ) : R

Finite q-Pochhammer symbol. $(a;q)_n = \prod_{k=0}^{n-1} (1 - a q^k)$.

Equations

• QSeries.qPochhammer a q n = ∏ k ∈ Finset.range n, (1 - a * q ^ k)

@[simp]

theorem QSeries.qPochhammer_zero {R : Type u_1} [CommRing R] (a q : R) : qPochhammer a q 0 = 1

The empty q-Pochhammer product $(a;q)_0 = 1$.

theorem QSeries.qPochhammer_succ {R : Type u_1} [CommRing R] (a q : R) (n : ℕ) : qPochhammer a q (n + 1) = qPochhammer a q n * (1 - a * q ^ n)

Recurrence for q-Pochhammer. $(a;q)_{n+1} = (a;q)_n \cdot (1 - a q^n)$.

def QSeries.qBinom {R : Type u_1} [CommRing R] : ℕ → ℕ → R → R

Gaussian binomial coefficient $\binom{n}{k}_q$.

Defined by the q-Pascal recurrence so that the result is always a polynomial in $q$ (no division). The boundary cases are $\binom{0}{0}_q = 1$, $\binom{0}{k+1}_q = 0$, $\binom{n+1}{0}_q = 1$.

Equations

• QSeries.qBinom 0 0 x✝ = 1
• QSeries.qBinom 0 n.succ x✝ = 0
• QSeries.qBinom n.succ 0 x✝ = 1
• QSeries.qBinom n.succ k.succ x✝ = QSeries.qBinom n (k + 1) x✝ + x✝ ^ (n - k) * QSeries.qBinom n k x✝

@[simp]

theorem QSeries.qBinom_zero_zero {R : Type u_1} [CommRing R] (q : R) : qBinom 0 0 q = 1

The Gaussian binomial coefficient $\binom{0}{0}_q = 1$.

@[simp]

theorem QSeries.qBinom_zero_succ {R : Type u_1} [CommRing R] (k : ℕ) (q : R) : qBinom 0 (k + 1) q = 0

The Gaussian binomial coefficient $\binom{0}{k+1}_q = 0$.

@[simp]

theorem QSeries.qBinom_succ_zero {R : Type u_1} [CommRing R] (n : ℕ) (q : R) : qBinom (n + 1) 0 q = 1

The Gaussian binomial coefficient $\binom{n+1}{0}_q = 1$.

@[simp]

theorem QSeries.qBinom_zero_right {R : Type u_1} [CommRing R] (n : ℕ) (q : R) : qBinom n 0 q = 1

The Gaussian binomial coefficient $\binom{n}{0}_q = 1$ for all $n$.

theorem QSeries.qBinom_succ_succ {R : Type u_1} [CommRing R] (n k : ℕ) (q : R) : qBinom (n + 1) (k + 1) q = qBinom n (k + 1) q + q ^ (n - k) * qBinom n k q

The q-Pascal recurrence $\binom{n+1}{k+1}_q = \binom{n}{k+1}_q + q^{n-k}\binom{n}{k}_q$.

theorem QSeries.qBinom_eq_zero_of_lt {R : Type u_1} [CommRing R] (q : R) {n k : ℕ} : n < k → qBinom n k q = 0

$\binom{n}{k}_q = 0$ whenever $k > n$.

theorem QSeries.qBinom_self {R : Type u_1} [CommRing R] (q : R) (n : ℕ) : qBinom n n q = 1

$\binom{n}{n}_q = 1$.

theorem QSeries.qBinom_mul_qPochhammer_mul_qPochhammer {R : Type u_1} [CommRing R] (q : R) {n k : ℕ} : k ≤ n → qBinom n k q * qPochhammer q q k * qPochhammer q q (n - k) = qPochhammer q q n

Closed-form identity. For $k \leq n$: $\binom{n}{k}_q (q;q)_k (q;q)_{n-k} = (q;q)_n$.