Digital binomial theorem

TheoremBase-\(b\) generalized digital binomial theorem#✓fully proved

Let \(b \ge 2\), let \(N\) and \(n\) be natural numbers with \(n < b^N\), and let \(x\) and \(y\) be real numbers. For a natural number \(m\) write \(m_i = \lfloor m / b^i \rfloor \bmod b\) for its \(i\)-th base-\(b\) digit, and write \(z^{\overline{j}} = z(z+1)\cdots(z+j-1)\) for the rising factorial. Then

\[\prod_{i=0}^{N-1} \frac{(x+y)^{\overline{n_i}}}{n_i!} = \sum_{m} \left(\prod_{i=0}^{N-1} \frac{x^{\overline{m_i}}}{m_i!}\right) \left(\prod_{i=0}^{N-1} \frac{y^{\overline{(n-m)_i}}}{(n-m)_i!}\right),\]

where the sum runs over the natural numbers \(m \le n\) with \(m_i \le n_i\) for every \(i < N\).

theorem base_b_generalized_digital_binomial_theorem
    (b N n : ℕ) (x y : ℝ) (hb : 2 ≤ b) (hn : n < b ^ N) :
    (∏ i ∈ Finset.range N,
      ((∏ j ∈ Finset.range (n / b ^ i % b), (x + y + (j : ℝ))) /
        ((n / b ^ i % b).factorial : ℝ)) =
      ∑ m ∈ Finset.filter
        (fun m => ∀ i ∈ Finset.range N, m / b ^ i % b ≤ n / b ^ i % b)
        (Finset.range (n + 1)),
        ((∏ i ∈ Finset.range N,
          ((∏ j ∈ Finset.range (m / b ^ i % b), (x + (j : ℝ))) /
            ((m / b ^ i % b).factorial : ℝ))) *
          (∏ i ∈ Finset.range N,
            ((∏ j ∈ Finset.range ((n - m) / b ^ i % b), (y + (j : ℝ))) /
              (((n - m) / b ^ i % b).factorial : ℝ)))))

Sources

Hieu D. Nguyen, "A Generalization of the Digital Binomial Theorem," Journal of Integer Sequences 18 (2015), Article 15.5.7, Theorem, equation (eq:digital-binomial-theorem-non-binary), lines 122–127, https://cs.uwaterloo.ca/journals/JIS/VOL18/Nguyen/nguyen6.tex

Uses 1

Proof usesBinomial theorem for rising factorials

DefinitionBinary digit sum#✓fully proved

For a natural number \(n\), the binary digit sum \(s(n)\) is the sum of the digits of \(n\) in base \(2\), that is, the number of ones in the binary expansion of \(n\).

def binDigitSum (n : ℕ) : ℕ := (Nat.digits 2 n).sum

Used by 7

Used byBinary digit sum of one · Binary digit sum of an even number · Binary digit sum of an odd number · Binary digit sum of zero · Digital binomial theorem · Digital binomial theorem over a commutative semiring · Tu–Deng conjecture

TheoremBinary digit sum of zero#✓fully proved

The binary digit sum of \(0\) is \(0\).

@[simp]
theorem binDigitSum_zero : binDigitSum 0 = 0

Uses 1 · Used by 3

Statement usesBinary digit sum

Used byBinary digit sum of one · Binary digit sum of an even number · Digital binomial theorem over a commutative semiring

TheoremBinary digit sum of an even number#✓fully proved

For every natural number \(k\), the binary digit sum of \(2k\) equals the binary digit sum of \(k\): doubling appends the binary digit \(0\).

@[simp]
theorem binDigitSum_two_mul (k : ℕ) : binDigitSum (2 * k) = binDigitSum k

Uses 2 · Used by 1

Statement usesBinary digit sum

Proof usesBinary digit sum of zero

Used byDigital binomial theorem over a commutative semiring

TheoremBinary digit sum of an odd number#✓fully proved

For every natural number \(k\), the binary digit sum of \(2k + 1\) is one more than the binary digit sum of \(k\): the binary expansion of \(2k + 1\) is that of \(k\) followed by the digit \(1\).

@[simp]
theorem binDigitSum_two_mul_add_one (k : ℕ) :
    binDigitSum (2 * k + 1) = binDigitSum k + 1

Uses 1 · Used by 2

Statement usesBinary digit sum

Used byBinary digit sum of one · Digital binomial theorem over a commutative semiring

TheoremBinary digit sum of one#✓fully proved

The binary digit sum of \(1\) is \(1\).

@[simp]
theorem binDigitSum_one : binDigitSum 1 = 1

Uses 3

Statement usesBinary digit sum

Proof usesBinary digit sum of an odd number · Binary digit sum of zero

TheoremDigital binomial theorem over a commutative semiring#✓fully proved

Let \(s(m)\) denote the binary digit sum of a natural number \(m\). For every natural number \(n\) and all elements \(x\), \(y\) of a commutative semiring, \((x + y)^{s(n)}\) equals the sum of \(x^{s(m)} y^{s(n - m)}\) over all \(m\) with \(0 \le m \le n\) and \(s(m) + s(n - m) = s(n)\).

theorem digital_binomial_theorem_general
    (n : ℕ) {R : Type*} [CommSemiring R] (x y : R) :
    (x + y) ^ binDigitSum n =
      ∑ m ∈ Finset.filter
        (fun m => binDigitSum m + binDigitSum (n - m) = binDigitSum n)
        (Finset.range (n + 1)),
        x ^ binDigitSum m * y ^ binDigitSum (n - m)

Uses 4 · Used by 1

Statement usesBinary digit sum

Proof usesBinary digit sum of an even number · Binary digit sum of an odd number · Binary digit sum of zero

Used byDigital binomial theorem

TheoremDigital binomial theorem#✓fully proved

Let \(s(m)\) denote the binary digit sum of a natural number \(m\). For every natural number \(n\) and all elements \(x\), \(y\) of a commutative ring, \((x + y)^{s(n)}\) equals the sum of \(x^{s(m)} y^{s(n - m)}\) over all \(m\) with \(0 \le m \le n\) and \(s(m) + s(n - m) = s(n)\).

The condition \(s(m) + s(n - m) = s(n)\) says that adding \(m\) and \(n - m\) in binary produces no carries; equivalently, \(m\) has a binary digit \(1\) only in positions where \(n\) has one.

theorem digital_binomial_theorem
    (n : ℕ) {R : Type*} [CommRing R] (x y : R) :
    (x + y) ^ binDigitSum n =
      ∑ m ∈ Finset.filter
        (fun m => binDigitSum m + binDigitSum (n - m) = binDigitSum n)
        (Finset.range (n + 1)),
        x ^ binDigitSum m * y ^ binDigitSum (n - m)

Sources

Hieu D. Nguyen, "A Generalization of the Digital Binomial Theorem," Journal of Integer Sequences 18 (2015), Article 15.5.7, Theorem, equation, lines 107–113, https://cs.uwaterloo.ca/journals/JIS/VOL18/Nguyen/nguyen6.tex

Uses 2

Statement usesBinary digit sum

Proof usesDigital binomial theorem over a commutative semiring

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.