Base-b digitwise binomial and multinomial coefficients

DefinitionThe \(b\)-ary binomial coefficient#✓fully proved

Let \(b \ge 2\) and let \(n\) and \(k\) be natural numbers with base-\(b\) digits \(n_l\) and \(k_l\), taken to be \(0\) beyond the last digit (with \(0\) having no digits). The \(b\)-ary binomial coefficient of \(n\) and \(k\) is \(\prod_{l=0}^{m-1} \binom{n_l}{k_l}\), where \(m\) is the larger of the numbers of base-\(b\) digits of \(n\) and of \(k\).

public def bAryBinomialCoefficient (b n k : Nat) (hb : 2 ≤ b) : Nat :=
  let _hb := hb
  let dn := Nat.digits b n
  let dk := Nat.digits b k
  let m := max dn.length dk.length
  ((List.range m).map (fun i => Nat.choose (dn.getD i 0) (dk.getD i 0))).foldl (· * ·) 1
Used by 9
Used byChu–Vandermonde identity for \(b\)-ary binomial coefficients · Digit-product formula for \(b\)-ary binomial coefficients · Digitwise product formula for the \(b\)-ary binomial coefficient · Generating function of the \(b\)-ary binomial coefficients · Pascal's recurrence for \(b\)-ary binomial coefficients · Symmetry of \(b\)-ary binomial coefficients · Symmetry and Pascal's recurrence for \(b\)-ary binomial coefficients · \(b\)-ary Chu–Vandermonde identity · Generating function of digitwise binomial products

TheoremDigitwise product formula for the \(b\)-ary binomial coefficient#✓fully proved

Let \(b \ge 2\), let \(n\) and \(k\) be natural numbers with base-\(b\) digits \(n_i\) and \(k_i\) (taken to be \(0\) beyond the last digit, and with \(0\) having no digits), and let \(L\) be at least the number of base-\(b\) digits of \(n\) and at least the number of base-\(b\) digits of \(k\). Then the \(b\)-ary binomial coefficient of \(n\) and \(k\) equals \(\prod_{i=0}^{L-1} \binom{n_i}{k_i}\).

theorem bAryBinomialCoefficient_eq_prod_getD (b n k : ℕ) (hb : 2 ≤ b) {L : ℕ}
    (hn : (Nat.digits b n).length ≤ L) (hk : (Nat.digits b k).length ≤ L) :
    bAryBinomialCoefficient b n k hb =
      ∏ i ∈ Finset.range L, ((Nat.digits b n).getD i 0).choose ((Nat.digits b k).getD i 0)
Uses 1 · Used by 3
Statement usesThe \(b\)-ary binomial coefficient
Used byDigit-product formula for \(b\)-ary binomial coefficients · Generating function of the \(b\)-ary binomial coefficients · Generating function of digitwise binomial products

TheoremGenerating function of the \(b\)-ary binomial coefficients#✓fully proved

Let \(R\) be a commutative semiring, let \(x \in R\), let \(b \ge 2\), and write \(\binom{n}{k}_b\) for the \(b\)-ary binomial coefficient of natural numbers \(n\) and \(k\). Let \(n\) have base-\(b\) digits \(n_0, \dots, n_{m-1}\), where \(m\) is the number of base-\(b\) digits of \(n\) (\(m = 0\) for \(n = 0\)). Then

\[ \sum_{k=0}^{n} \binom{n}{k}_b x^k = \prod_{l=0}^{m-1} \left(1 + x^{b^l}\right)^{n_l}. \]
theorem bAryBinomialCoefficient_generating_function {R : Type*} [CommSemiring R] (b n : ℕ)
    (x : R) (hb : 2 ≤ b) :
    ∑ k ∈ Finset.range (n + 1), (bAryBinomialCoefficient b n k hb : R) * x ^ k =
      ∏ l ∈ Finset.range (Nat.digits b n).length,
        (1 + x ^ (b ^ l)) ^ ((Nat.digits b n).getD l 0)
Sources
  • Lin Jiu and Christophe Vignat, "On Binomial Identities in Arbitrary Bases," Journal of Integer Sequences 19 (2016), Article 16.5.5, Theorem (equation eq:barybinomialgeneratingfunction), lines 322–329, https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu4.tex
Uses 2 · Used by 2
Statement usesThe \(b\)-ary binomial coefficient
Proof usesDigitwise product formula for the \(b\)-ary binomial coefficient
Used byChu–Vandermonde identity for \(b\)-ary binomial coefficients · Generating function of digitwise binomial products

TheoremGenerating function of digitwise binomial products#✓fully proved

Let \(R\) be a commutative ring, let \(x \in R\), let \(b \ge 2\), and let \(n\) have base-\(b\) digits \(n_0, \dots, n_{m-1}\), where \(m\) is the number of base-\(b\) digits of \(n\) (\(m = 0\) for \(n = 0\)). For each natural number \(k\) let \(k_l\) be its \(l\)-th base-\(b\) digit, taken to be \(0\) beyond the last digit. Then

\[ \sum_{k=0}^{n} \Bigl(\prod_{l=0}^{m-1} \binom{n_l}{k_l}\Bigr) x^k = \prod_{l=0}^{m-1} \left(1 + x^{b^l}\right)^{n_l}. \]

The product \(\prod_{l=0}^{m-1} \binom{n_l}{k_l}\) is the \(b\)-ary binomial coefficient of \(n\) and \(k\) whenever \(k \le n\).

theorem base_digits_binomial_generating_function
    {R : Type*} [CommRing R] (b n : ℕ) (x : R) (hb : 2 ≤ b) :
    ∑ k ∈ Finset.range (n + 1),
        (∏ l ∈ Finset.range (Nat.digits b n).length,
          (((Nat.digits b n).getD l 0).choose ((Nat.digits b k).getD l 0) : R)) * x ^ k =
    ∏ l ∈ Finset.range (Nat.digits b n).length,
      (1 + x ^ (b ^ l)) ^ ((Nat.digits b n).getD l 0)
Sources
  • Lin Jiu and Christophe Vignat, "On Binomial Identities in Arbitrary Bases," Journal of Integer Sequences 19 (2016), Article 16.5.5, Theorem (equation eq:barybinomialgeneratingfunction), lines 322–329, https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu4.tex
Uses 3
Proof usesThe \(b\)-ary binomial coefficient · Digitwise product formula for the \(b\)-ary binomial coefficient · Generating function of the \(b\)-ary binomial coefficients

TheoremDigit-product formula for \(b\)-ary binomial coefficients#✓fully proved

Let \(b \ge 2\) and let \(n\), \(k\) and \(L\) be natural numbers with \(n < b^L\) and \(k < b^L\). Then the \(b\)-ary binomial coefficient \(\binom{n}{k}_b\) equals

\[\prod_{i=0}^{L-1} \binom{\lfloor n / b^i \rfloor \bmod b}{\lfloor k / b^i \rfloor \bmod b},\]

the product over the positions \(i < L\) of the binomial coefficients of the \(i\)-th base-\(b\) digits of \(n\) and \(k\).

theorem bAryBinomialCoefficient_eq_prod_div_pow (b n k : ℕ) (hb : 2 ≤ b) {L : ℕ}
    (hn : n < b ^ L) (hk : k < b ^ L) :
    bAryBinomialCoefficient b n k hb =
      ∏ i ∈ Finset.range L, Nat.choose ((n / b ^ i) % b) ((k / b ^ i) % b)
Uses 2 · Used by 5
Statement usesThe \(b\)-ary binomial coefficient
Proof usesDigitwise product formula for the \(b\)-ary binomial coefficient
Used byChu–Vandermonde identity for \(b\)-ary binomial coefficients · Pascal's recurrence for \(b\)-ary binomial coefficients · Symmetry of \(b\)-ary binomial coefficients · Symmetry and Pascal's recurrence for \(b\)-ary binomial coefficients · \(b\)-ary Chu–Vandermonde identity

TheoremSymmetry of \(b\)-ary binomial coefficients#✓fully proved

Let \(b \ge 2\) and write \(\binom{n}{k}_b\) for the \(b\)-ary binomial coefficient. For all natural numbers \(k \le n\), \(\binom{n}{k}_b = \binom{n}{n-k}_b\).

theorem bAryBinomialCoefficient_symm (b n k : ℕ) (hb : 2 ≤ b) (hkn : k ≤ n) :
    bAryBinomialCoefficient b n k hb = bAryBinomialCoefficient b n (n - k) hb
Uses 2 · Used by 1
Statement usesThe \(b\)-ary binomial coefficient
Proof usesDigit-product formula for \(b\)-ary binomial coefficients
Used bySymmetry and Pascal's recurrence for \(b\)-ary binomial coefficients

TheoremPascal's recurrence for \(b\)-ary binomial coefficients#✓fully proved

Let \(b \ge 2\) and write \(\binom{n}{k}_b\) for the \(b\)-ary binomial coefficient. For all natural numbers \(n\) and \(k\) with \(0 < k \le n\) and \(\binom{n}{k}_b \ne 0\), \(\binom{n}{k}_b = \binom{n-1}{k-1}_b + \binom{n-1}{k}_b\).

theorem bAryBinomialCoefficient_pascal (b n k : ℕ) (hb : 2 ≤ b) (hk : 0 < k) (hkn : k ≤ n)
    (hne : bAryBinomialCoefficient b n k hb ≠ 0) :
    bAryBinomialCoefficient b n k hb =
      bAryBinomialCoefficient b (n - 1) (k - 1) hb + bAryBinomialCoefficient b (n - 1) k hb
Uses 2 · Used by 1
Statement usesThe \(b\)-ary binomial coefficient
Proof usesDigit-product formula for \(b\)-ary binomial coefficients
Used bySymmetry and Pascal's recurrence for \(b\)-ary binomial coefficients

TheoremSymmetry and Pascal's recurrence for \(b\)-ary binomial coefficients#✓fully proved

Let \(b \ge 2\). For a natural number \(m\) write \(m_i = \lfloor m / b^i \rfloor \bmod b\) for its \(i\)-th base-\(b\) digit. For integers \(m\) and \(j\), let \(C_b(m, j) = \prod_{i=0}^{m+j} \binom{m_i}{j_i}\) if \(m \ge 0\) and \(j \ge 0\), and \(C_b(m, j) = 0\) otherwise. Then for all integers \(n\) and \(k\) with \(0 < n\) and \(0 \le k \le n\), we have \(C_b(n, k) = C_b(n, n - k)\), and if \(C_b(n, k) \ne 0\) then \(C_b(n, k) = C_b(n - 1, k - 1) + C_b(n - 1, k)\).

theorem baryBinomial_symmetry_and_pascal
    (b : ℕ) (hb : 2 ≤ b) (n k : ℤ) (hn : 0 < n) (hk : 0 ≤ k) (hkn : k ≤ n) :
    let baryBinomial : ℤ → ℤ → ℕ := fun m j =>
      if 0 ≤ m ∧ 0 ≤ j then
        let m' := m.toNat
        let j' := j.toNat
        ∏ i ∈ Finset.range (m' + j' + 1),
          Nat.choose ((m' / b ^ i) % b) ((j' / b ^ i) % b)
      else
        0
    baryBinomial n k = baryBinomial n (n - k) ∧
      (baryBinomial n k ≠ 0 →
        baryBinomial n k =
          baryBinomial (n - 1) (k - 1) + baryBinomial (n - 1) k)
Sources
  • Lin Jiu and Christophe Vignat, "On Binomial Identities in Arbitrary Bases," Journal of Integer Sequences 19 (2016), Article 16.5.5, Theorem (Symmetry and recurrence), equation, lines 432–445, https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu4.tex
Uses 4
Proof usesThe \(b\)-ary binomial coefficient · Digit-product formula for \(b\)-ary binomial coefficients · Pascal's recurrence for \(b\)-ary binomial coefficients · Symmetry of \(b\)-ary binomial coefficients

TheoremChu–Vandermonde identity for \(b\)-ary binomial coefficients#✓fully proved

Let \(b \ge 2\) and write \(\binom{n}{k}_b\) for the \(b\)-ary binomial coefficient. Let \(m\) and \(n\) be natural numbers that add without carries in base \(b\), that is, \(\lfloor m / b^l \rfloor \bmod b + \lfloor n / b^l \rfloor \bmod b < b\) for every natural number \(l\). Then for every natural number \(r\),

\[\binom{m+n}{r}_b = \sum_{k=0}^{r} \binom{m}{k}_b \binom{n}{r-k}_b.\]
theorem bAryBinomialCoefficient_chu_vandermonde (b m n r : ℕ) (hb : 2 ≤ b)
    (hcarry : ∀ l, (m / b ^ l) % b + (n / b ^ l) % b < b) :
    bAryBinomialCoefficient b (m + n) r hb =
      ∑ k ∈ Finset.range (r + 1),
        bAryBinomialCoefficient b m k hb * bAryBinomialCoefficient b n (r - k) hb
Uses 3 · Used by 1
Statement usesThe \(b\)-ary binomial coefficient
Proof usesDigit-product formula for \(b\)-ary binomial coefficients · Generating function of the \(b\)-ary binomial coefficients
Used by\(b\)-ary Chu–Vandermonde identity

Theorem\(b\)-ary Chu–Vandermonde identity#✓fully proved

Let \(b \ge 2\). For a natural number \(x\) write \(x_l = \lfloor x / b^l \rfloor \bmod b\) for its \(l\)-th base-\(b\) digit, and for natural numbers \(x\) and \(y\) let \(C(x, y) = \prod_{l=0}^{x+y} \binom{x_l}{y_l}\). Let \(m\), \(n\) and \(r\) be natural numbers such that the addition of \(m\) and \(n\) in base \(b\) has no carries, that is, \(m_l + n_l < b\) for every \(l \le m + n\). Then

\[C(m + n, r) = \sum_{k=0}^{r} C(m, k)\, C(n, r - k).\]

The product \(C(x, y)\) is the \(b\)-ary binomial coefficient \(\binom{x}{y}_b\).

theorem bary_chu_vandermonde (b m n r : ℕ) (hb : 2 ≤ b)
    (hcarry : ∀ l ∈ Finset.range (m + n + 1), (m / b ^ l) % b + (n / b ^ l) % b < b) :
    (let C : ℕ → ℕ → ℕ := fun x y =>
      ∏ l ∈ Finset.range (x + y + 1),
        Nat.choose ((x / b ^ l) % b) ((y / b ^ l) % b);
      C (m + n) r = ∑ k ∈ Finset.range (r + 1), C m k * C n (r - k))
Sources
  • Lin Jiu and Christophe Vignat, "On Binomial Identities in Arbitrary Bases," Journal of Integer Sequences 19 (2016), Article 16.5.5, Theorem (equation bChuVandermonde), lines 371–377, https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu4.tex
Uses 3
Proof usesThe \(b\)-ary binomial coefficient · Chu–Vandermonde identity for \(b\)-ary binomial coefficients · Digit-product formula for \(b\)-ary binomial coefficients

DefinitionBase-\(b\) digit of a natural number#✓fully proved

For natural numbers \(b\), \(n\) and \(l\), the rank-\(l\) base-\(b\) digit \(n_l\) of \(n\) is the entry at position \(l\) (counting from \(0\)) of the list of base-\(b\) digits of \(n\), least significant digit first, and \(0\) when \(l\) is at least the length of that list (with \(0\) having no digits). For \(b \ge 2\) this is the coefficient of \(b^l\) in the base-\(b\) expansion of \(n\).

For \(b \le 1\) the digit list follows Mathlib's convention: for \(b = 0\) a positive \(n\) has the single digit \(n\), and for \(b = 1\) the digits of \(n\) are \(n\) ones.

public def bAryDigit (b n l : ℕ) : ℕ := (Nat.digits b n).getD l 0
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu3.tex, lines 349-359.
Used by 2
Used byRank-\(l\) base-\(b\) digits of a list · Digitwise \(b\)-ary multinomial factor

DefinitionRank-\(l\) base-\(b\) digits of a list#✓fully proved

For natural numbers \(b\) and \(l\) and a list \((k_1, \dots, k_m)\) of natural numbers, this is the list \(((k_1)_l, \dots, (k_m)_l)\), where \((k_i)_l\) is the rank-\(l\) base-\(b\) digit of \(k_i\).

public def bAryLowerDigits (b : ℕ) (ks : List ℕ) (l : ℕ) : List ℕ :=
  ks.map (fun k => bAryDigit b k l)
Uses 1 · Used by 1
Statement usesBase-\(b\) digit of a natural number
Used byDigitwise \(b\)-ary multinomial factor

DefinitionMultinomial coefficient with a prescribed top#✓fully proved

For a natural number \(t\) and a list \((a_1, \dots, a_m)\) of natural numbers, the multinomial factor of \(t\) over \((a_1, \dots, a_m)\) is \(\frac{t!}{a_1! \cdots a_m!}\) if \(a_1 + \dots + a_m = t\), and \(0\) otherwise.

public def ordinaryMultinomialFactor (top : ℕ) (lowers : List ℕ) : ℕ :=
  if lowers.sum = top then lowers.multinomial else 0
Used by 1
Used byDigitwise \(b\)-ary multinomial factor

DefinitionDigitwise \(b\)-ary multinomial factor#✓fully proved

For natural numbers \(b\), \(n\) and \(l\) and a list \((k_1, \dots, k_m)\) of natural numbers, let \(n_l\) and \((k_i)_l\) be the rank-\(l\) base-\(b\) digits of \(n\) and \(k_i\). The factor at rank \(l\) is \(\frac{n_l!}{(k_1)_l! \cdots (k_m)_l!}\) if \((k_1)_l + \dots + (k_m)_l = n_l\), and \(0\) otherwise.

public def bAryMultinomialFactor (b n : ℕ) (ks : List ℕ) (l : ℕ) : ℕ :=
  ordinaryMultinomialFactor (bAryDigit b n l) (bAryLowerDigits b ks l)
Uses 3 · Used by 1
Statement usesBase-\(b\) digit of a natural number · Rank-\(l\) base-\(b\) digits of a list · Multinomial coefficient with a prescribed top
Used byThe \(b\)-ary multinomial coefficient

DefinitionDigit-length bound for the \(b\)-ary multinomial coefficient#✓fully proved

For natural numbers \(b\) and \(n\) and a list \((k_1, \dots, k_m)\) of natural numbers, the bound is the largest of the numbers of base-\(b\) digits of \(n, k_1, \dots, k_m\) (with \(0\) having no digits).

Every nonzero base-\(b\) digit of \(n\) and of each \(k_i\) has rank below the bound, so at every higher rank the digitwise \(b\)-ary multinomial factor equals \(1\); this plays the role of the source's sufficiently large \(N\).

public def bAryMultinomialBound (b n : ℕ) (ks : List ℕ) : ℕ :=
  max ((Nat.digits b n).length)
    (((ks.map (fun k => (Nat.digits b k).length)).max?).getD 0)
Used by 1
Used byThe \(b\)-ary multinomial coefficient

DefinitionThe \(b\)-ary multinomial coefficient#✓fully proved

Let \(b \ge 2\), let \(n\) be a natural number and let \((k_1, \dots, k_m)\) be a list of natural numbers, and write \(n_l\) and \((k_i)_l\) for the rank-\(l\) base-\(b\) digits of \(n\) and \(k_i\) (taken to be \(0\) beyond the last digit, with \(0\) having no digits). Let \(N\) be the largest of the numbers of base-\(b\) digits of \(n, k_1, \dots, k_m\). The \(b\)-ary multinomial coefficient of \(n\) over \((k_1, \dots, k_m)\) is \(\prod_{l=0}^{N-1} c_l\), where \(c_l = \frac{n_l!}{(k_1)_l! \cdots (k_m)_l!}\) if \((k_1)_l + \dots + (k_m)_l = n_l\) and \(c_l = 0\) otherwise.

public def bAryMultinomial (b n : ℕ) (ks : List ℕ) (hb : 2 ≤ b) : ℕ :=
  let _ : 2 ≤ b := hb
  (Finset.range (bAryMultinomialBound b n ks)).prod
    (fun l => bAryMultinomialFactor b n ks l)
Sources
  • https://cs.uwaterloo.ca/journals/JIS/VOL19/Jiu/jiu3.tex, lines 349-359.
Uses 2
Statement usesDigit-length bound for the \(b\)-ary multinomial coefficient · Digitwise \(b\)-ary multinomial factor
16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.