Multiple harmonic sums

TheoremDilcher's finite multiple harmonic identity for every exponent#✓fully proved

For every natural number \(m\) (including \(m = 0\)) and every positive integer \(n\),

\[ \sum_{k=1}^{n} \frac{(-1)^{k-1} \binom{n}{k}}{k^m} = \sum_{1 \le j_1 \le \cdots \le j_m \le n} \frac{1}{j_1 \cdots j_m}, \]

where the right side sums over all weakly increasing tuples \((j_1, \ldots, j_m)\) of integers between \(1\) and \(n\); for \(m = 0\) there is only the empty tuple, whose term is \(1\).

theorem dilcher_finite_multiple_harmonic_identity_general (m n : ℕ) (hn : 0 < n) :
    (∑ k ∈ Finset.Icc 1 n,
      ((n.choose k : ℚ) * (-1 : ℚ) ^ (k - 1)) / (k : ℚ) ^ m) =
    ∑ js ∈ Finset.univ.filter
      (fun js : Fin m → Fin n => Monotone (fun i => (js i).val)),
      (∏ i, ((js i).val + 1 : ℚ))⁻¹
Used by 1
Used byDilcher's finite multiple harmonic identity

TheoremDilcher's finite multiple harmonic identity#✓fully proved

For all positive integers \(m\) and \(n\),

\[ \sum_{k=1}^{n} \frac{(-1)^{k-1} \binom{n}{k}}{k^m} = \sum_{1 \le j_1 \le \cdots \le j_m \le n} \frac{1}{j_1 \cdots j_m}, \]

where the right side sums over all weakly increasing tuples \((j_1, \ldots, j_m)\) of integers between \(1\) and \(n\).

theorem dilcher_finite_multiple_harmonic_identity (m n : ℕ)
    (hm : 0 < m) (hn : 0 < n) :
    (∑ k ∈ Finset.Icc 1 n,
      ((n.choose k : ℚ) * (-1 : ℚ) ^ (k - 1)) / (k : ℚ) ^ m) =
    ∑ js ∈ Finset.univ.filter
      (fun js : Fin m → Fin n => Monotone (fun i => (js i).val)),
      (∏ i, ((js i).val + 1 : ℚ))⁻¹
Sources
  • Khristo N. Boyadzhiev, "Harmonic Number Identities Via Euler's Transform", Journal of Integer Sequences 12 (2009), Article 09.6.1, https://cs.uwaterloo.ca/journals/JIS/VOL12/Boyadzhiev/boyadzhiev3.tex, controlling statement equation (26), lines 323–331. Boyadzhiev attributes the identity to Karl Dilcher, "Some q-series identities related to divisor functions", Discrete Mathematics 145 (1995), 83–93, DOI 10.1016/0012-365X(95)00092-B (the JIS bibliography prints "divisor factors").
Uses 1
Proof usesDilcher's finite multiple harmonic identity for every exponent

DefinitionMultiple harmonic sums#✓fully proved

For natural numbers \(p\), \(r\) and \(n\), the multiple harmonic sum \(H_r^{(n)}\) modulo \(p\) is the element

\[H_r^{(n)} = \sum_{0 < k_1 < \cdots < k_n \le r} k_1^{-1} \cdots k_n^{-1}\]

of \(\mathbb{Z}/p\mathbb{Z}\), where the sum runs over the strictly increasing \(n\)-tuples of integers, equivalently over the \(n\)-element subsets of \(\{1, \dots, r\}\), and \(k^{-1}\) is the inverse of \(k\) in \(\mathbb{Z}/p\mathbb{Z}\) (Mathlib's total inverse, which is the true inverse whenever \(k\) is a unit modulo \(p\)). In particular \(H_r^{(0)} = 1\), and \(H_r^{(n)} = 0\) when \(n > r\).

def multipleHarmonic (p r n : ℕ) : ZMod p :=
  ∑ s ∈ (Finset.Icc 1 r).powersetCard n, ∏ i ∈ s, ((i : ZMod p))⁻¹
Sources
Used by 1
Used byMattarei–Tauraso polynomial congruence for multiple harmonic sums

TheoremMattarei–Tauraso polynomial congruence for multiple harmonic sums#✓fully proved

Let \(n \ge 1\) and let \(p\) be a prime with \(p > n + 1\), write \(H_r^{(m)}\) for the multiple harmonic sum modulo \(p\), and write \(k^{-1}\) for the inverse of \(k\) in \(\mathbb{Z}/p\mathbb{Z}\). Then, as polynomials in \(x\) over \(\mathbb{Z}/p\mathbb{Z}\),

\[\sum_{k=1}^{p-1} H_{k-1}^{(n-1)} k^{-1} x^k = (-1)^{n-1} \sum_{k=1}^{p-1} (k^{-1})^n (1 - x)^k.\]
theorem multiple_harmonic_polynomial_congruence (n p : ℕ) (hn : 0 < n)
    (hp : p.Prime) (hpp : n + 1 < p) :
    (∑ k ∈ Finset.Icc 1 (p - 1),
      Polynomial.C (multipleHarmonic p (k - 1) (n - 1) * (((k : ZMod p))⁻¹)) *
        (Polynomial.X : Polynomial (ZMod p)) ^ k) =
    Polynomial.C ((-1 : ZMod p) ^ (n - 1)) *
      ∑ k ∈ Finset.Icc 1 (p - 1),
        Polynomial.C (((((k : ZMod p))⁻¹) ^ n)) *
          (1 - (Polynomial.X : Polynomial (ZMod p))) ^ k
Sources
Uses 1
Statement usesMultiple harmonic sums
4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.