Dixon's identity

TheoremDixon's alternating cubic binomial sum#✓fully proved

For every natural number \(n\), \(\sum_{k=0}^{2n} (-1)^k \binom{2n}{k}^3 = (-1)^n \binom{2n}{n} \binom{3n}{2n}\).

Mikić attributes the identity to A. C. Dixon, "On the sum of the cubes of the coefficients in a certain expansion by the binomial theorem", Messenger of Mathematics 20 (1891), 79--80. This is the specialization of Dixon's three-parameter identity in which all three parameters equal \(n\); the three-parameter identity is not stated.

theorem dixon_alternating_cubic_binomial_sum (n : ℕ) :
    ∑ k ∈ Finset.range (2 * n + 1),
      (-1 : ℤ) ^ k * (Nat.choose (2 * n) k : ℤ) ^ 3 =
      (-1 : ℤ) ^ n * (Nat.choose (2 * n) n : ℤ) *
        (Nat.choose (3 * n) (2 * n) : ℤ)
Sources

DefinitionExtended factorial#✓fully proved

For an integer \(n\), the extended factorial of \(n\) is the rational number \(n!\) when \(n \ge 0\) and \(0\) when \(n < 0\).

public def extFact (n : ℤ) : ℚ :=
  if 0 ≤ n then (n.natAbs.factorial : ℚ) else 0
Used by 7
Used byDixon's summation theorem · The extended factorial of a natural number · The extended factorial vanishes at negative integers · Integer binomial coefficient · Integer binomial coefficients of natural numbers · Integer binomial coefficients vanish when the lower index exceeds the upper · Integer binomial coefficients vanish at negative lower index

TheoremThe extended factorial vanishes at negative integers#✓fully proved

For every integer \(n < 0\), the extended factorial of \(n\) is \(0\).

@[simp] public theorem extFact_of_neg {n : ℤ} (hn : n < 0) : extFact n = 0
Uses 1 · Used by 1
Statement usesExtended factorial
Used byDixon's summation theorem

TheoremThe extended factorial of a natural number#✓fully proved

For every natural number \(n\), the extended factorial of \(n\) equals the ordinary factorial \(n!\).

@[simp] public theorem extFact_natCast (n : ℕ) : extFact n = n.factorial
Uses 1 · Used by 1
Statement usesExtended factorial
Used byInteger binomial coefficients of natural numbers

DefinitionInverse factorial on the integers#✓fully proved

For an integer \(n\), the inverse factorial of \(n\) is the rational number \(1/n!\) when \(n \ge 0\) and \(0\) when \(n < 0\).

public def invFact (n : ℤ) : ℚ :=
  if 0 ≤ n then 1 / (n.natAbs.factorial : ℚ) else 0
Used by 8
Used byDixon's summation theorem · Integer binomial coefficient · Integer binomial coefficients of natural numbers · Integer binomial coefficients vanish when the lower index exceeds the upper · Integer binomial coefficients vanish at negative lower index · The inverse factorial at natural numbers · The inverse factorial vanishes at negative integers · Shift identity for the inverse factorial

TheoremThe inverse factorial vanishes at negative integers#✓fully proved

For every integer \(n < 0\), the inverse factorial of \(n\) is \(0\).

@[simp] public theorem invFact_of_neg {n : ℤ} (hn : n < 0) : invFact n = 0
Uses 1 · Used by 3
Statement usesInverse factorial on the integers
Used byDixon's summation theorem · Integer binomial coefficients vanish when the lower index exceeds the upper · Integer binomial coefficients vanish at negative lower index

TheoremThe inverse factorial at natural numbers#✓fully proved

For every natural number \(n\), the inverse factorial of \(n\), viewed as an integer, equals \((n!)^{-1}\) in \(\mathbb{Q}\).

@[simp] public theorem invFact_natCast (n : ℕ) : invFact n = (n.factorial : ℚ)⁻¹
Uses 1 · Used by 1
Statement usesInverse factorial on the integers
Used byInteger binomial coefficients of natural numbers

TheoremShift identity for the inverse factorial#✓fully proved

For every integer \(n\), the inverse factorial of \(n\) equals \(n + 1\) times the inverse factorial of \(n + 1\), as rational numbers.

For \(n \ge 0\) this is \(1/n! = (n+1)/(n+1)!\). For \(n < 0\) both sides are \(0\): the inverse factorial vanishes at negative integers, and the factor \(n + 1\) is \(0\) at \(n = -1\).

public theorem invFact_shift (n : ℤ) : invFact n = (n + 1) * invFact (n + 1)
Uses 1 · Used by 1
Statement usesInverse factorial on the integers
Used byDixon's summation theorem

DefinitionInteger binomial coefficient#✓fully proved

For an integer \(m\) write \(m!\) for the extended factorial and \(\frac{1}{m!}\) for the inverse factorial; both are \(0\) when \(m < 0\). For integers \(n\) and \(k\), the integer binomial coefficient is the rational number \(\binom{n}{k} = n! \cdot \frac{1}{k!} \cdot \frac{1}{(n - k)!}\).

These are the source's zero conventions: \(\binom{n}{k} = 0\) unless \(0 \le k \le n\).

public def intBinom (n k : ℤ) : ℚ :=
  extFact n * invFact k * invFact (n - k)
Uses 2 · Used by 5
Statement usesExtended factorial · Inverse factorial on the integers
Used byTerm of Dixon's alternating sum · Dixon's summation theorem · Integer binomial coefficients of natural numbers · Integer binomial coefficients vanish when the lower index exceeds the upper · Integer binomial coefficients vanish at negative lower index

TheoremInteger binomial coefficients of natural numbers#✓fully proved

For natural numbers \(k \le n\), the integer binomial coefficient of \(n\) and \(k\) equals the ordinary binomial coefficient \(\binom{n}{k}\).

@[simp] public theorem intBinom_natCast {n k : ℕ} (hk : k ≤ n) :
    intBinom n k = n.choose k
Uses 5
Statement usesInteger binomial coefficient
Proof usesExtended factorial · The extended factorial of a natural number · Inverse factorial on the integers · The inverse factorial at natural numbers

TheoremInteger binomial coefficients vanish at negative lower index#✓fully proved

For integers \(n\) and \(k\) with \(k < 0\), the integer binomial coefficient \(\binom{n}{k}\) is \(0\).

@[simp] public theorem intBinom_of_neg_right {n k : ℤ} (hk : k < 0) : intBinom n k = 0
Uses 4
Statement usesInteger binomial coefficient
Proof usesExtended factorial · Inverse factorial on the integers · The inverse factorial vanishes at negative integers

TheoremInteger binomial coefficients vanish when the lower index exceeds the upper#✓fully proved

For integers \(n < k\), the integer binomial coefficient \(\binom{n}{k}\) is \(0\).

@[simp] public theorem intBinom_of_lt {n k : ℤ} (h : n < k) : intBinom n k = 0
Uses 4
Statement usesInteger binomial coefficient
Proof usesExtended factorial · Inverse factorial on the integers · The inverse factorial vanishes at negative integers

DefinitionTerm of Dixon's alternating sum#✓fully proved

Write \(\binom{n}{m}\) for the integer binomial coefficient of integers \(n\) and \(m\). For integers \(a_1, a_2, a_3\) and \(k\), the Dixon summand is the rational number \((-1)^k \binom{2a_1}{a_1 + k} \binom{2a_2}{a_2 + k} \binom{2a_3}{a_3 + k}\).

public def dixonSummand (a₁ a₂ a₃ k : ℤ) : ℚ :=
  (-1 : ℚ) ^ k.natAbs * intBinom (2 * a₁) (a₁ + k) *
    (intBinom (2 * a₂) (a₂ + k) * intBinom (2 * a₃) (a₃ + k))
Uses 1 · Used by 2
Statement usesInteger binomial coefficient
Used byDixon's summation theorem · The Dixon sum \(\upsilon_3\)

DefinitionBound of the Dixon summation window#✓fully proved

For integers \(a_1, a_2, a_3\), the Dixon bound is \(\max(|a_1|, |a_2|, |a_3|)\).

Every integer \(k\) whose term in Dixon's alternating sum is nonzero satisfies \(|k|\) at most this bound, so summing over \(k\) from minus the bound to the bound covers the whole sum.

public def dixonBound (a₁ a₂ a₃ : ℤ) : ℤ :=
  max (|a₁|) (max (|a₂|) (|a₃|))
Used by 2
Used byDixon's summation theorem · The Dixon sum \(\upsilon_3\)

DefinitionThe Dixon sum \(\upsilon_3\)#✓fully proved

For integers \(a_1, a_2, a_3\), let \(B = \max(|a_1|, |a_2|, |a_3|)\). Then \(\upsilon_3(a_1, a_2, a_3)\) is the rational number

\[\upsilon_3(a_1, a_2, a_3) = \sum_{k=-B}^{B} (-1)^k \prod_{i=1}^{3} \binom{2a_i}{a_i + k},\]

where for integers \(n\) and \(k\) the binomial coefficient \(\binom{n}{k}\) is the ordinary one when \(0 \le k \le n\) and is \(0\) otherwise.

Every summand with \(|k| > B\) is zero, so this is the alternating sum over all integers \(k\).

public def upsilon₃ (a₁ a₂ a₃ : ℤ) : ℚ :=
  ∑ k ∈ Finset.Icc (-(dixonBound a₁ a₂ a₃)) (dixonBound a₁ a₂ a₃),
    dixonSummand a₁ a₂ a₃ k
Uses 2 · Used by 1
Statement usesBound of the Dixon summation window · Term of Dixon's alternating sum
Used byDixon's summation theorem

TheoremDixon's summation theorem#✓fully proved

For an integer \(m\) write \(m!\) for the extended factorial and \(\frac{1}{m!}\) for the inverse factorial; both are \(0\) when \(m < 0\). For all integers \(a_1, a_2, a_3\), the Dixon sum \(\Upsilon_3(a_1, a_2, a_3)\) equals

\[ (2a_1)!\,(2a_2)!\,(2a_3)!\,(a_1 + a_2 + a_3)! \cdot \frac{1}{(a_1 + a_2)!} \cdot \frac{1}{(a_1 + a_3)!} \cdot \frac{1}{(a_2 + a_3)!} \cdot \frac{1}{a_1!} \cdot \frac{1}{a_2!} \cdot \frac{1}{a_3!}. \]

Proof: a Wilf–Zeilberger pair. For \(a = a_1 \ge 0\) and \(b = a_2 \ge 0\) the normalized summand in \(c = a_3\) has the certificate ratio \(R(c, k) = -\frac{(a + k)(b + k)}{2(c - k + 1)(a + b + c + 1)}\); induction on \(c\) telescopes over the fixed window \([-a, a]\). Negative arguments make both sides zero.

public theorem dixon_summation (a₁ a₂ a₃ : ℤ) :
  upsilon₃ a₁ a₂ a₃ =
    extFact (2 * a₁) * extFact (2 * a₂) * extFact (2 * a₃) *
      extFact (a₁ + a₂ + a₃) * invFact (a₁ + a₂) * invFact (a₁ + a₃) *
      invFact (a₂ + a₃) * invFact a₁ * invFact a₂ * invFact a₃
Sources
  • Abdesselam, arXiv:1903.11147v2, Proposition (Dixon), TeX lines 502-512.
Uses 9
Statement usesExtended factorial · Inverse factorial on the integers · The Dixon sum \(\upsilon_3\)
Proof usesBound of the Dixon summation window · Term of Dixon's alternating sum · The extended factorial vanishes at negative integers · Integer binomial coefficient · The inverse factorial vanishes at negative integers · Shift identity for the inverse factorial
16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.