Binomial sums and hypergeometric identities

Evaluations and bounds of sums of products of binomial coefficients: Chu–Vandermonde, Dixon, Knuth's old sum, Staver, Frisch, Klamkin, hockey-stick and Filipponi identities, partial-sum bounds, multisection identities, and Franel, Domb, Zagier and Catalan–Larcombe–French numbers defined by binomial sums.

TheoremA binomial double sum equal to a power of two minus a Fibonacci number#✓fully proved

For every natural number \(n\),

\[\sum_{k=0}^{\lfloor n/2 \rfloor} \sum_{q=0}^{n-2k} \binom{n-k}{q} = 2^{n+1} - F_{n+2},\]

where \(F_m\) is the \(m\)-th Fibonacci number, with \(F_0 = 0\) and \(F_1 = 1\).

theorem binomial_double_sum_eq_pow_sub_fib (n : ℕ) :
    (∑ k ∈ Finset.range (n / 2 + 1),
      ∑ q ∈ Finset.range (n - 2 * k + 1), Nat.choose (n - k) q) =
      2 ^ (n + 1) - Nat.fib (n + 2)
Sources
  • Denis Neiter and Amsha Proag, "Links Between Sums Over Paths in Bernoulli's Triangles and the Fibonacci Numbers," Journal of Integer Sequences 19 (2016), Article 16.8.3, Theorem, lines 247–252, https://cs.uwaterloo.ca/journals/JIS/VOL19/Proag/proag3.tex

TheoremAlternating binomial sums of partial sums#✓fully proved

For every sequence \(a_0, a_1, a_2, \dots\) of complex numbers and every natural number \(n\),

\[\sum_{k=0}^{n} (-1)^k \binom{n}{k} \sum_{j=1}^{k} a_j = \sum_{k=0}^{n-1} (-1)^{k+1} \binom{n-1}{k} a_{k+1},\]

where an empty sum is \(0\), so both sides vanish when \(n = 0\).

theorem alternating_binomial_partial_sum
    (a : ℕ → ℂ) (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1),
      (-1 : ℂ) ^ k * (Nat.choose n k : ℂ) * (∑ j ∈ Finset.Icc 1 k, a j)) =
    ∑ k ∈ Finset.range n,
      (-1 : ℂ) ^ (k + 1) * (Nat.choose (n - 1) k : ℂ) * a (k + 1)
Sources
  • Necdet Batır and Anthony Sofo, "A Unified Treatment of Certain Classes of Combinatorial Identities," Journal of Integer Sequences 24 (2021), Article 21.3.2, Theorem A.

DefinitionCatalan–Larcombe–French numbers#✓fully proved

For a natural number \(n\), the \(n\)th Catalan–Larcombe–French number (OEIS A053175) is

\[ P_n = 2^n \sum_{k=0}^{n} \binom{n}{2k} \binom{2k}{k}^2 4^{n-2k}, \]

where the terms with \(2k > n\) vanish because \(\binom{n}{2k} = 0\).

public def catalanLarcombeFrenchNumber : ℕ → ℕ :=
  fun n => 2 ^ n * Finset.sum (Finset.range (n + 1)) fun k =>
    Nat.choose n (2 * k) * Nat.choose (2 * k) k ^ 2 * 4 ^ (n - 2 * k)

TheoremGeneralized hockey stick identity of Lynch and Weselcouch#●ready to prove

For all natural numbers \(n\) and \(k\),

\[\sum_{i=0}^{k} \binom{2i + n}{i} = \sum_{i=0}^{\lfloor k/2 \rfloor} (-1)^i \binom{2k + 1 + n - i}{k - 2i}.\]
theorem_wanted sum_choose_two_mul_add (n k : ℕ) :
    (∑ i ∈ Finset.range (k + 1),
        (Nat.choose (2 * i + n) i : ℤ)) =
      ∑ i ∈ Finset.range (k / 2 + 1),
        (-1 : ℤ) ^ i *
          (Nat.choose (2 * k + 1 + n - i) (k - 2 * i) : ℤ)
Sources
  • Molly Lynch and Michael Weselcouch, "A Generalized Hockey Stick Theorem", Corollary 15.

TheoremStrehl's identity for the Franel numbers#✓fully proved

For every natural number \(n\),

\[\sum_{k=0}^{n} \binom{n}{k}^2 \binom{2k}{n} = \sum_{k=0}^{n} \binom{n}{k}^3,\]

where the right-hand side is the \(n\)-th Franel number.

theorem strehl_franel_binomial_identity (n : ℕ) :
    (∑ k ∈ Finset.range (n + 1), (Nat.choose n k) ^ 2 * Nat.choose (2 * k) n) =
      ∑ k ∈ Finset.range (n + 1), (Nat.choose n k) ^ 3
Sources
  • Sela Fried, Proofs of Ten Conjectures From the OEIS, Journal of Integer Sequences 29 (2026), Article 26.1.8, equation 1est, lines 110–114, https://cs.uwaterloo.ca/journals/JIS/VOL29/Fried/fried21.tex, recalling V. Strehl, Binomial identities — combinatorial and algorithmic aspects, Discrete Math. 136 (1994), formula (29).

TheoremTerminating Chu–Vandermonde specialization#✓fully proved

For every natural number \(n \ge 1\), the following sum of rational numbers vanishes:

\[\sum_{k=0}^{n} \binom{n}{k} \binom{n+k}{k} \frac{(-1)^k}{k+1} = 0.\]

The source identifies the sum as the terminating Gauss hypergeometric value \({}_2F_1(n+1, -n; 2; 1) = (1-n)_n / (2)_n = 0\), where \((a)_n\) is the rising factorial.

theorem chu_vandermonde_terminating_specialization
    (n : ℕ) (hn : 1 ≤ n) :
    ∑ k ∈ Finset.range (n + 1),
      (n.choose k : ℚ) * ((n + k).choose k : ℚ) * (-1 : ℚ) ^ k / (k + 1) = 0
Sources
5 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.