Ward's generalized binomial coefficients

DefinitionUnits-place carry#✓fully proved

For natural numbers \(b\), \(n\) and \(m\), the units-place carry \(\varepsilon_0^{b,n,m}\) of \(n + m\) in base \(b\) is \(1\) if \(b > 1\) and \((n \bmod b) + (m \bmod b) \ge b\), and \(0\) otherwise; in particular it is \(0\) for the invalid bases \(b \le 1\).

public def wardUnitsCarry (b n m : ℕ) : ℕ :=
  if 1 < b ∧ b ≤ n % b + m % b then 1 else 0

Used by 3

Used byWard generalized binomial coefficient · Ward's generalized binomial coefficient as a finite product · Units-place carry as a quotient

DefinitionWard generalized binomial coefficient#✓fully proved

Let \(R\) be a commutative monoid and \(s = (s_b)_{b \in \mathbb{N}}\) a sequence in \(R\). For natural numbers \(n\) and \(m\), the Ward generalized binomial coefficient is

\[\binom{n+m}{n}_s = \prod_{b=2}^{n+m} s_b^{\varepsilon_0^{b,n,m}},\]

where \(\varepsilon_0^{b,n,m} \in \{0, 1\}\) is the carry in the units place when \(n\) and \(m\) are added in base \(b\).

This is Ward's product \(\prod_{b > 1} s_b^{\varepsilon_0^{b,n,m}}\): no base larger than \(n + m\) carries in the units place, so the product is finite. The source uses the product as a definition for arbitrary coefficient sequences, including sequences with zero terms.

public def wardGeneralizedBinomialCoefficient {R : Type*} [CommMonoid R]
    (s : ℕ → R) (n m : ℕ) : R :=
  ((Finset.range (n + m + 1)).filter fun b => 1 < b).prod
    fun b => s b ^ wardUnitsCarry b n m

Uses 1 · Used by 3

Statement usesUnits-place carry

Used byWard's generalized binomial coefficient as a finite product · Ward's identity for generalized binomial coefficients · Ward's identity with hypotheses at positive indices

TheoremUnits-place carry as a quotient#✓fully proved

For all natural numbers \(b\), \(n\) and \(m\), the units-place carry of \(n + m\) in base \(b\) (taken to be \(0\) when \(b \le 1\)) equals \(\lfloor ((n \bmod b) + (m \bmod b)) / b \rfloor\), where \(n \bmod 0 = n\) and division by \(0\) gives \(0\).

theorem wardUnitsCarry_eq_div (b n m : ℕ) : wardUnitsCarry b n m = (n % b + m % b) / b

Uses 1 · Used by 1

Statement usesUnits-place carry

Used byWard's generalized binomial coefficient as a finite product

TheoremWard's generalized binomial coefficient as a finite product#✓fully proved

Let \(R\) be a commutative monoid and \(s = (s_b)_{b \in \mathbb{N}}\) a sequence in \(R\). For all natural numbers \(n\) and \(m\), the Ward generalized binomial coefficient \(\binom{n+m}{n}_s\) equals

\[\prod_{b=2}^{n+m} s_b^{\lfloor ((n \bmod b) + (m \bmod b)) / b \rfloor}.\]

theorem wardGeneralizedBinomialCoefficient_eq_prod_Icc {R : Type*} [CommMonoid R]
    (s : ℕ → R) (n m : ℕ) :
    wardGeneralizedBinomialCoefficient s n m =
      ∏ b ∈ Finset.Icc 2 (n + m), s b ^ ((n % b + m % b) / b)

Uses 3 · Used by 2

Statement usesWard generalized binomial coefficient

Proof usesUnits-place carry · Units-place carry as a quotient

Used byWard's identity for generalized binomial coefficients · Ward's identity with hypotheses at positive indices

TheoremWard's identity with hypotheses at positive indices#✓fully proved

Let \(s, f : \mathbb{N} \to \mathbb{Z}\) satisfy \(s(b) \ne 0\) for every \(b \ge 1\) and \(f(k) = \prod_{d \mid k} s(d)\) for every \(k \ge 1\), the product running over the positive divisors of \(k\). Write \(f!(t) = \prod_{i=1}^{t} f(i)\). Let \(n\) and \(m\) be natural numbers, and let \(\binom{n+m}{n}_s\) be the Ward generalized binomial coefficient of \(s\) at \(n\) and \(m\). Then the identity

\[\frac{f!(n+m)}{f!(n) \, f!(m)} = \binom{n+m}{n}_s\]

holds in \(\mathbb{Q}\).

theorem ward_sbinomial_carry_product_general
    (s : ℕ → ℤ) (hs : ∀ b, 0 < b → s b ≠ 0)
    (f : ℕ → ℤ) (hf : ∀ k, 0 < k → f k = ∏ d ∈ Nat.divisors k, s d)
    (n m : ℕ) :
    ((∏ i ∈ Finset.Icc 1 (n + m), f i : ℤ) : ℚ) /
        (((∏ i ∈ Finset.Icc 1 n, f i : ℤ) : ℚ) * ((∏ i ∈ Finset.Icc 1 m, f i : ℤ) : ℚ)) =
      ((wardGeneralizedBinomialCoefficient s n m : ℤ) : ℚ)

Uses 2 · Used by 1

Statement usesWard generalized binomial coefficient

Proof usesWard's generalized binomial coefficient as a finite product

Used byWard's identity for generalized binomial coefficients

TheoremWard's identity for generalized binomial coefficients#✓fully proved

Let \(s, f : \mathbb{N} \to \mathbb{Z}\) satisfy \(s(b) \ne 0\) for every natural number \(b\) and \(f(k) = \prod_{d \mid k} s(d)\) for every natural number \(k\), the product running over the positive divisors of \(k\) (empty for \(k = 0\)). Write \(f!(t) = \prod_{i=1}^{t} f(i)\). Then for all natural numbers \(n\) and \(m\), the identity

\[\frac{f!(n+m)}{f!(n) \, f!(m)} = \prod_{b=2}^{n+m} s(b)^{\lfloor ((n \bmod b) + (m \bmod b)) / b \rfloor}\]

holds in \(\mathbb{Q}\).

The exponent \(\lfloor ((n \bmod b) + (m \bmod b)) / b \rfloor\) is the carry in the ones position when adding \(n\) and \(m\) in base \(b\); for the classical case this recovers Kummer's carry-count theorem.

theorem ward_sbinomial_carry_product
    (s : Nat → Int) (hs : ∀ b, s b ≠ 0)
    (f : Nat → Int) (hf : ∀ k, f k = ∏ d ∈ Nat.divisors k, s d)
    (n m : Nat) :
    let fFactorial : Nat → Int := fun t => ∏ i ∈ Finset.Icc 1 t, f i;
    (fFactorial (n + m) : ℚ) / ((fFactorial n : ℚ) * (fFactorial m : ℚ)) =
      ∏ b ∈ Finset.Icc 2 (n + m), (s b : ℚ) ^ ((n % b + m % b) / b)

Sources

• Tom Edgar and Michael Z. Spivey, "Multiplicative Functions, Generalized Binomial Coefficients, and Generalized Catalan Numbers," Journal of Integer Sequences 19 (2016), Article 16.1.6, Theorem [Ward] thmward (equation wardeqn), lines 475–482, https://cs.uwaterloo.ca/journals/JIS/VOL19/Edgar/edgar3.tex; attributed there to M. Ward.

Uses 3

Proof usesWard generalized binomial coefficient · Ward's generalized binomial coefficient as a finite product · Ward's identity with hypotheses at positive indices

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.