Binomial sums involving absolute values

TheoremBrent–Osborn binomial absolute moment identity#✓fully proved

For every natural number \(n\),

\[\sum_{k=0}^{2n} \sum_{\ell=0}^{2n} \binom{2n}{k} \binom{2n}{\ell} \, \bigl| (k-n)^2 - (\ell-n)^2 \bigr| = 2n^2 \binom{2n}{n}^2.\]

In centered form this says \(\sum_{k,\ell} \binom{2n}{n+k} \binom{2n}{n+\ell} \, |k^2 - \ell^2| = 2n^2 \binom{2n}{n}^2\), the sum running over all integers \(k, \ell\), since the binomial coefficients vanish for \(|k| > n\).

theorem brent_osborn_binomial_absolute_moment (n : ℕ) :
    (∑ k : Fin (2 * n + 1), ∑ l : Fin (2 * n + 1),
      Nat.choose (2 * n) k.1 * Nat.choose (2 * n) l.1 *
        Int.natAbs (((k.1 : ℤ) - n) ^ 2 - ((l.1 : ℤ) - n) ^ 2)) =
      2 * n ^ 2 * (Nat.choose (2 * n) n) ^ 2
Sources
  • Richard P. Brent, Hideyuki Ohtsuka, Judy-anne H. Osborn, and Helmut Prodinger, "Some Binomial Sums Involving Absolute Values," Journal of Integer Sequences 19 (2016), Article 16.3.7, Theorem [Brent and Osborn], lines 377–383 (with the W_β definition at lines 345–349), https://cs.uwaterloo.ca/journals/JIS/VOL19/Brent/brent9.tex

TheoremReduction of a double binomial absolute-value sum#✓fully proved

For all natural numbers \(\beta\), \(m\) and \(n\),

\[\sum_{i=0}^{2m} \sum_{j=0}^{2n} \binom{2m}{i} \binom{2n}{j} \lvert (i-m)-(j-n) \rvert^{\beta} = \sum_{k=0}^{2(m+n)} \binom{2(m+n)}{k} \lvert k-m-n \rvert^{\beta},\]

with the convention \(0^0 = 1\).

In the source's notation, \(S_\beta(n) = \sum_k \binom{2n}{n+k} \lvert k \rvert^\beta\) and \(T_\beta(m,n) = \sum_{k,\ell} \binom{2m}{m+k} \binom{2n}{n+\ell} \lvert k-\ell \rvert^\beta\), and the identity reads \(T_\beta(m,n) = S_\beta(m+n)\), after the shift \(i = m + k\), \(j = n + \ell\).

theorem double_binomial_sum_eq_single_binomial_sum
    (β m n : ℕ) :
    Finset.sum (Finset.range (2 * m + 1)) (fun i =>
      Finset.sum (Finset.range (2 * n + 1)) (fun j =>
        Nat.choose (2 * m) i * Nat.choose (2 * n) j *
          Int.natAbs ((i : ℤ) - (m : ℤ) - ((j : ℤ) - (n : ℤ))) ^ β)) =
      Finset.sum (Finset.range (2 * (m + n) + 1)) (fun k =>
        Nat.choose (2 * (m + n)) k *
          Int.natAbs ((k : ℤ) - (m : ℤ) - (n : ℤ)) ^ β)
Sources
  • Richard P. Brent, Hideyuki Ohtsuka, Judy-anne H. Osborn, and Helmut Prodinger, "Some Binomial Sums Involving Absolute Values," Journal of Integer Sequences 19 (2016), Article 16.3.7, Theorem, lines 278–283 (with S_β defined at lines 245–247 and T_β at 271–274), https://cs.uwaterloo.ca/journals/JIS/VOL19/Brent/brent9.tex
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.