b-nomial coefficients

DefinitionBase polynomial of the \(b\)-nomial coefficients#✓fully proved

For a natural number \(b \ge 2\), this is the integer polynomial \(1 + X + \dots + X^{b-1} = \sum_{i=0}^{b-1} X^i \in \mathbb{Z}[X]\).

noncomputable def bNomialBase (b : ℕ) (_hb : 2 ≤ b) : Polynomial ℤ :=
  ∑ i ∈ Finset.range b, X ^ i

Used by 1

Used byType-1 \(b\)-nomial coefficients

DefinitionType-1 \(b\)-nomial coefficients#✓fully proved

For natural numbers \(b \ge 2\) and \(n\) and an integer \(k\), the type-1 \(b\)-nomial coefficient in row \(n\) and column \(k\) is the coefficient of \(X^k\) in \((1 + X + \dots + X^{b-1})^n \in \mathbb{Z}[X]\) when \(k \ge 0\), and \(0\) when \(k < 0\).

noncomputable def bNomialCoefficient (b : ℕ) (hb : 2 ≤ b) (n : ℕ) (k : ℤ) : ℤ :=
  if k < 0 then 0 else ((bNomialBase b hb) ^ n).coeff k.toNat

Uses 1

Statement usesBase polynomial of the \(b\)-nomial coefficients

DefinitionDigits of a string extended by zero#✓fully proved

For a \(b\)-ary string \(x = (x_0, \dots, x_{n-1})\) of length \(n\), written from left to right, and a natural number \(j\), this is the digit \(x_j\) if \(j < n\), and \(0\) if \(j \ge n\).

Positions in \(x\) run from left to right, so \(x_0\) represents the source's leftmost digit \(a_n\). In particular, position \(n\) represents the stipulated boundary digit \(a_0 = 0\).

def bNomialDigitAtOrZero {n b : ℕ} (x : Fin n → Fin b) (j : ℕ) : ℕ :=
  if h : j < n then (x ⟨j, h⟩).val else 0

Used by 2

Used byNumber of indispensable digits · Indispensable digits

DefinitionIndispensable digits#✓fully proved

Let \(x = (x_0, \dots, x_{n-1})\) be a \(b\)-ary string of length \(n\), written from left to right, and extend it by zero on the right, setting \(x_j = 0\) for \(j \ge n\). A position \(p < n\) is indispensable in \(x\) when there is a natural number \(r\) with \(1 \le r \le n + 1 - p\) such that \(x_{p+t} = x_p\) for every \(t\) with \(1 \le t < r\), and \(x_{p+r} < x_p\). That is, some nonempty constant run of digits beginning at position \(p\) is followed on the right by a strictly smaller digit.

The paper writes the digit at position \(p\) as \(a_i\) with \(i = n - p\) and prints the witness bound \(r \le i + 1\), although only the boundary digit \(a_0\) (position \(n\)) is defined. With the zero extension the final case \(r = i + 1\) is unsatisfiable, so the predicate agrees with the source in every case the source defines.

def IsBNomialIndispensableDigit {n b : ℕ} (x : Fin n → Fin b) (p : Fin n) : Prop :=
  ∃ r : Fin (n + 2),
    1 ≤ r.val ∧
      p.val + r.val ≤ n + 1 ∧
      (∀ t : Fin (n + 2), 1 ≤ t.val → t.val < r.val →
        bNomialDigitAtOrZero x (p.val + t.val) = (x p).val) ∧
      bNomialDigitAtOrZero x (p.val + r.val) < (x p).val

Uses 1 · Used by 1

Statement usesDigits of a string extended by zero

Used byNumber of indispensable digits

DefinitionNumber of indispensable digits#✓fully proved

For a \(b\)-ary string \(x\) of finite length, \(\iota(x)\) is the number of positions of \(x\) that are indispensable.

def bNomialIndispensableDigitCount {n b : ℕ} (x : Fin n → Fin b) : ℕ :=
  Fintype.card { p : Fin n // IsBNomialIndispensableDigit x p }

Uses 2 · Used by 1

Statement usesIndispensable digits · Digits of a string extended by zero

Used byType-3 b-nomial numbers

DefinitionType-3 b-nomial numbers#✓fully proved

For a natural number \(b \ge 2\), a natural number \(n\) and an integer \(k\), the type-3 \(b\)-nomial number is the number of \(b\)-ary strings \(x\) of length \(n\) with exactly \(k\) indispensable digits, that is, with \(\iota(x) = k\). In particular it is zero for \(k < 0\).

At \(n = 0\) this gives the source convention: the value is one at \(k = 0\) and zero otherwise.

def bNomialNumberType3 (b : ℕ) (_hb : 2 ≤ b) (n : ℕ) (k : ℤ) : ℕ :=
  Fintype.card { x : Fin n → Fin b // (bNomialIndispensableDigitCount x : ℤ) = k }

Uses 1

Statement usesNumber of indispensable digits

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.