Binomial identities for harmonic numbers

TheoremAlternating binomial transform of the harmonic numbers#✓fully proved

Let \(s\) be a complex number that is not a negative integer, let \(n\) be a positive integer, and let \(H_k = \sum_{j=1}^{k} 1/j\) be the \(k\)-th harmonic number. For complex \(z\) and natural \(k\) write \(\binom{z}{k} = \Gamma(z + 1) / (\Gamma(k + 1)\,\Gamma(z - k + 1))\), with \(1/\Gamma\) taken to be \(0\) at the poles of \(\Gamma\). Then

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

The generalized binomial coefficients are written as Gamma-function quotients, and the assumption that \(s\) is not a negative integer is the source condition \(s \in \mathbb{C} \setminus \mathbb{Z}^-\).

MetaMathlibExt.alternating_binomial_transform_harmonic_numbers · 17 lines

theorem alternating_binomial_transform_harmonic_numbers (s : ℂ) (n : ℕ)
    (hs : ∀ m : ℕ, s ≠ -((m + 1 : ℕ) : ℂ)) (hn : 0 < n) :
    ∑ k ∈ Finset.Icc 1 n,
      ((-1 : ℂ) ^ k *
        (Complex.Gamma (((n : ℂ) + s) + 1) /
          (Complex.Gamma ((k : ℂ) + 1) * Complex.Gamma (((n : ℂ) + s) - (k : ℂ) + 1))) *
        ((harmonic k : ℚ) : ℂ)) =
      (-1 : ℂ) ^ n *
          (Complex.Gamma ((s + (n : ℂ) - 1) + 1) /
            (Complex.Gamma ((n : ℂ) + 1) *
              Complex.Gamma ((s + (n : ℂ) - 1) - (n : ℂ) + 1))) *
          ((harmonic n : ℚ) : ℂ) +
        ((-1 : ℂ) ^ n / (s + (n : ℂ))) *
          (Complex.Gamma ((s + (n : ℂ) - 1) + 1) /
            (Complex.Gamma ((n : ℂ) + 1) *
              Complex.Gamma ((s + (n : ℂ) - 1) - (n : ℂ) + 1))) -
        1 / (s + (n : ℂ))

Sources

• Necdet Batır, "Finite Binomial Sum Identities with Harmonic Numbers," Journal of Integer Sequences 24 (2021), Article 21.4.3, Corollary 3, lines 220–226, https://cs.uwaterloo.ca/journals/JIS/VOL24/Batir2/batir13.tex

TheoremBinomial-harmonic convolution identity#✓fully proved

Let \(H_m = \sum_{i=1}^{m} 1/i\) denote the \(m\)-th harmonic number. For natural numbers \(k\) and \(n\) with \(1 \le k \le n\),

\[\sum_{\nu=1}^{n} \left(\binom{n+k-\nu-1}{n-1} - \binom{n+k-\nu-1}{k-1}\right) H_\nu = \binom{n+k}{k} (H_k - H_n).\]

theorem binomial_harmonic_convolution (k n : ℕ) (hk : 0 < k) (hkn : k ≤ n) :
    ∑ ν ∈ Finset.Icc 1 n,
      (((Nat.choose (n + k - ν - 1) (n - 1) : ℚ) -
        (Nat.choose (n + k - ν - 1) (k - 1) : ℚ)) * harmonic ν) =
      (Nat.choose (n + k) k : ℚ) * (harmonic k - harmonic n)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers," Journal of Integer Sequences 29 (2026), Article 26.4.8, Theorem 1, equation (1.1), lines 135–141, https://cs.uwaterloo.ca/journals/JIS/VOL29/Alzer/alzer22.tex

TheoremBinomial interchange identity with harmonic weights#✓fully proved

Let \(K\) be a field of characteristic zero. For every natural number \(n\) and every sequence \(a : \mathbb{N} \to K\),

\[\sum_{k=1}^{n} \frac{1}{k} \sum_{j=1}^{k} \binom{k}{j} a_j = \sum_{k=1}^{n} \binom{n}{k} \frac{a_k}{k}.\]

The source notes a generalization in Boyadzhiev, attributed to 't Woord. The statement generalizes the source's real or complex sequences to any field of characteristic zero.

theorem binomial_harmonic_interchange_identity {K : Type*} [Field K] [CharZero K]
    (n : ℕ) (a : ℕ → K) :
  Finset.sum (Finset.Icc 1 n)
    (fun k => (1 / (k : K)) *
      Finset.sum (Finset.Icc 1 k) (fun j => (Nat.choose k j : K) * a j)) =
  Finset.sum (Finset.Icc 1 n) (fun k => (Nat.choose n k : K) * a k / (k : K))

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, Lemma A, lines 150–156, https://cs.uwaterloo.ca/journals/JIS/VOL24/Batir/batir7.tex

TheoremAlternating binomial transform of second-order harmonic numbers#✓fully proved

For a natural number \(m\) let \(H_m = \sum_{j=1}^{m} 1/j\) and \(H_m^{(2)} = \sum_{j=1}^{m} 1/j^2\), and for \(z \in \mathbb{C}\) and a natural number \(r\) let \(\binom{z}{r} = z(z-1)\cdots(z-r+1)/r!\), the empty product for \(r = 0\) being \(1\). Let \(s \in \mathbb{C}\) with \(s \ne -m\) for every positive integer \(m\), and let \(n \ge 1\). Then

\[\sum_{k=1}^{n} (-1)^k \binom{s+n}{k} H_k^{(2)} = (-1)^n \binom{s+n-1}{n} H_n^{(2)} - \frac{1}{s+n} \Bigl(H_n - s \sum_{k=1}^{n} \frac{(-1)^k \binom{s+k-1}{k-1}}{k^2 \binom{n}{k}}\Bigr).\]

MetaMathlibExt.binomial_transform_second_order_harmonic_numbers · 20 lines

theorem binomial_transform_second_order_harmonic_numbers
    (s : ℂ) (n : ℕ) (hn : 0 < n)
    (hs : ∀ m : ℕ, s ≠ -((m + 1 : ℕ) : ℂ)) :
    (∑ k ∈ Finset.Icc 1 n,
        (-1 : ℂ) ^ k *
          ((Finset.range k).prod (fun j => s + (n : ℂ) - (j : ℂ)) /
            (Nat.factorial k : ℂ)) *
          (∑ j ∈ Finset.Icc 1 k, (1 : ℂ) / (j : ℂ) ^ 2)) =
      (-1 : ℂ) ^ n *
          ((Finset.range n).prod (fun j => s + (n : ℂ) - 1 - (j : ℂ)) /
            (Nat.factorial n : ℂ)) *
          (∑ j ∈ Finset.Icc 1 n, (1 : ℂ) / (j : ℂ) ^ 2) -
        1 / (s + (n : ℂ)) *
          ((∑ j ∈ Finset.Icc 1 n, (1 : ℂ) / (j : ℂ)) -
            s * ∑ k ∈ Finset.Icc 1 n,
              ((-1 : ℂ) ^ k *
                  ((Finset.range (k - 1)).prod
                      (fun j => s + (k : ℂ) - 1 - (j : ℂ)) /
                    (Nat.factorial (k - 1) : ℂ))) /
                ((k : ℂ) ^ 2 * (n.choose k : ℂ)))

Sources

• Necdet Batır, "Finite Binomial Sum Identities with Harmonic Numbers," Journal of Integer Sequences 24 (2021), Article 21.4.3, Proposition 6, equation (2.8), lines 260–267, https://cs.uwaterloo.ca/journals/JIS/VOL24/Batir2/batir13.tex

TheoremAlternating binomial transform of the squared harmonic numbers#✓fully proved

For a complex number \(z\) and \(k \in \mathbb{N}\) write \(\binom{z}{k} = z(z-1)\cdots(z-k+1)/k!\) (the empty product being \(1\)), and let \(H_k = 1 + \frac{1}{2} + \cdots + \frac{1}{k}\) be the \(k\)-th harmonic number. Let \(s\) be a complex number that is not a negative integer, and let \(n \ge 1\). Then

\[ \sum_{k=1}^{n} (-1)^k \binom{s+n}{k} H_k^2 = (-1)^n \binom{s+n-1}{n} \left(H_n^2 + \frac{2 H_n}{s+n} + \frac{2}{(s+n)^2}\right) + \frac{H_n}{s+n} - \frac{2}{(s+n)^2} - \frac{s}{s+n} \sum_{k=1}^{n} \frac{(-1)^k \binom{s+k-1}{k-1}}{k^2 \binom{n}{k}}. \]

theorem binomial_transform_sq_harmonic (s : ℂ) (n : ℕ)
    (hs : ∀ m : ℕ, s ≠ -((m : ℂ) + 1)) (hn : 0 < n) :
  ∑ k ∈ Finset.Icc 1 n,
      ((-1 : ℂ) ^ k * ((descPochhammer ℂ k).eval (s + (n : ℂ)) / (k.factorial : ℂ)) *
        (harmonic k : ℂ) ^ 2) =
    (-1 : ℂ) ^ n * ((descPochhammer ℂ n).eval (s + (n : ℂ) - 1) / (n.factorial : ℂ)) *
        ((harmonic n : ℂ) ^ 2 + 2 * (harmonic n : ℂ) / (s + (n : ℂ)) +
          2 / (s + (n : ℂ)) ^ 2) +
      (harmonic n : ℂ) / (s + (n : ℂ)) - 2 / (s + (n : ℂ)) ^ 2 -
      s / (s + (n : ℂ)) *
        ∑ k ∈ Finset.Icc 1 n,
          (((-1 : ℂ) ^ k * ((descPochhammer ℂ (k - 1)).eval (s + (k : ℂ) - 1) /
            ((k - 1).factorial : ℂ))) / ((k : ℂ) ^ 2 * (Nat.choose n k : ℂ)))

Sources

• Necdet Batır, "Finite Binomial Sum Identities with Harmonic Numbers," Journal of Integer Sequences 24 (2021), Article 21.4.3, Theorem 7, equation (2.12), lines 287–293, https://cs.uwaterloo.ca/journals/JIS/VOL24/Batir2/batir13.tex

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.