Quadrinomial coefficients

DefinitionQuadrinomial coefficient triangle#✓fully proved

For natural numbers \(n\) and \(k\), the quadrinomial coefficient \(\binom{n}{k}_4\) is the coefficient of \(x^k\) in the polynomial \((1 + x + x^2 + x^3)^n\) with natural-number coefficients. These numbers form the triangle OEIS A008287.

noncomputable def polynomialQuadrinomialCoeff (n k : ℕ) : ℕ :=
  ((1 + Polynomial.X + Polynomial.X ^ 2 + Polynomial.X ^ 3 : Polynomial ℕ) ^ n).coeff k

DefinitionZhang's six-parameter binomial sum#✓fully proved

For natural numbers \(n\), \(r_1\), \(r_2\), \(s\), \(t\), \(u\), Zhang's binomial sum is

\[ V(n, r_1, r_2, s, t, u) = \sum_{k=0}^{n} \binom{n}{k}^{r_1} \binom{n}{2k}^{r_2} \binom{n+k}{k}^{s} \binom{2k}{k}^{t} \binom{2(n-k)}{n-k}^{u}. \]

The source uses the convention \(0^0 = 1\), which is also Lean's convention for natural-number powers.

def zhangVSum (n r₁ r₂ s t u : ℕ) : ℕ :=
  ∑ k ∈ Finset.range (n + 1),
    n.choose k ^ r₁ * n.choose (2 * k) ^ r₂ *
      ((n + k).choose k ^ s * ((2 * k).choose k ^ t * (2 * (n - k)).choose (n - k) ^ u))

Used by 1

Used byQuadrinomial numbers as a specialization of Zhang's V-sum

DefinitionQuadrinomial sequence A005725#✓fully proved

For a natural number \(n\), the quadrinomial number is \(Q(n) = \sum_{k=0}^{n} \binom{n}{k} \binom{n}{2k}\). This is OEIS sequence A005725.

def quadrinomialCoeff (n : ℕ) : ℕ :=
  ∑ k ∈ Finset.range (n + 1), n.choose k * n.choose (2 * k)

Used by 1

Used byQuadrinomial numbers as a specialization of Zhang's V-sum

TheoremQuadrinomial numbers as a specialization of Zhang's V-sum#✓fully proved

For every natural number \(n\), the quadrinomial number \(Q(n) = \sum_{k=0}^{n} \binom{n}{k} \binom{n}{2k}\) equals Zhang's six-parameter binomial sum \(V(n, 1, 1, 0, 0, 0)\).

theorem quadrinomialCoeff_eq_zhangVSum (n : ℕ) :
    quadrinomialCoeff n = zhangVSum n 1 1 0 0 0

Uses 2

Statement usesQuadrinomial sequence A005725 · Zhang's six-parameter binomial sum

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.