Binomial sums involving absolute values
TheoremBrent–Osborn binomial absolute moment identity#✓fully proved
MetaMathlibExt.brent_osborn_binomial_absolute_moment
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
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
MetaMathlibExt.double_binomial_sum_eq_single_binomial_sum
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
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 andT_βat 271–274), https://cs.uwaterloo.ca/journals/JIS/VOL19/Brent/brent9.tex
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.