Ramanujan's binomial–harmonic identity

TheoremShifted binomial–harmonic convolution (Alzer–Kwong, Corollary 1)#●ready to prove

For natural numbers \(k\) and \(n\) with \(2 \le k \le n\),

\[ \sum_{\nu=1}^{n+1} \Bigl(\binom{n+k-\nu-1}{n} - \binom{n+k-\nu-1}{k-2}\Bigr) H_\nu = \binom{n+k}{k-1} (H_k - H_{n+1}) - \frac{1}{n+1} \binom{n+k}{k}, \]

where \(H_m = \sum_{j=1}^{m} 1/j\) is the \(m\)-th harmonic number.

theorem_wanted sum_choose_sub_choose_mul_harmonic_succ_eq
    (k n : ℕ) (hk : 2 ≤ k) (hkn : k ≤ n) :
    ∑ ν ∈ Finset.Icc 1 (n + 1),
        ((Nat.choose (n + k - ν - 1) n : ℚ) -
          (Nat.choose (n + k - ν - 1) (k - 2) : ℚ)) * harmonic ν =
      (Nat.choose (n + k) (k - 1) : ℚ) *
          (harmonic k - harmonic (n + 1)) -
        (1 / ((n : ℚ) + 1)) * (Nat.choose (n + k) k : ℚ)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Corollary 1.

TheoremShifted binomial–harmonic convolution (Alzer–Kwong, Corollary 2)#●ready to prove

For natural numbers \(k\) and \(n\) with \(1 \le k \le n - 1\),

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

where \(H_m = \sum_{j=1}^{m} 1/j\) is the \(m\)-th harmonic number.

theorem_wanted sum_choose_sub_choose_mul_harmonic_eq_add
    (k n : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n - 1) :
    ∑ ν ∈ Finset.Icc 1 n,
        ((Nat.choose (n + k - ν - 1) (n - 2) : ℚ) -
          (Nat.choose (n + k - ν - 1) k : ℚ)) * harmonic ν =
      (Nat.choose (n + k) (k + 1) : ℚ) * (harmonic k - harmonic n) +
        (1 / ((k : ℚ) + 1)) * (Nat.choose (n + k + 1) (k + 1) : ℚ)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Corollary 2.

TheoremRamanujan's binomial sine series#●ready to prove

Let \(a\), \(N\) and \(\theta\) be real numbers with \(N \ge 0\) and \(|\theta| \le \pi / 2\). Then the series \(\sum_{\nu=0}^{\infty} \binom{N}{\nu} \sin((a + 2\nu)\theta)\) converges unconditionally to \(2^N (\cos \theta)^N \sin((a + N)\theta)\). Here \(\binom{N}{\nu} = N(N-1)\cdots(N-\nu+1)/\nu!\) is the generalized binomial coefficient, and \(2^N\) and \((\cos \theta)^N\) are real powers.

theorem_wanted hasSum_ringChoose_mul_sin
    (a N θ : ℝ) (hN : 0 ≤ N) (hθ : |θ| ≤ Real.pi / 2) :
    HasSum
      (fun ν : ℕ => Ring.choose N ν * Real.sin ((a + 2 * (ν : ℝ)) * θ))
      ((2 : ℝ) ^ N * (Real.cos θ) ^ N * Real.sin ((a + N) * θ))

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Lemma 1.

TheoremThe Rung-Obaid trigonometric identity#●ready to prove

Let \(k\) and \(n\) be natural numbers with \(1 \le k \le n\), and let \(\theta\) be a real number. Then

\[\sum_{\nu=1}^{n} 2^\nu \left( \binom{n+k-\nu-1}{k-1} - \binom{n+k-\nu-1}{n-1} \right) \cos^\nu \theta \, \sin(\nu\theta) = 2^{n+k} \cos^{n+k} \theta \, \sin((n-k)\theta).\]

theorem_wanted sum_two_pow_choose_sub_mul_cos_pow_sin
    (k n : ℕ) (hk : 1 ≤ k) (hkn : k ≤ n) (θ : ℝ) :
    ∑ ν ∈ Finset.Icc 1 n,
        (2 : ℝ) ^ ν *
          ((Nat.choose (n + k - ν - 1) (k - 1) : ℝ) -
            (Nat.choose (n + k - ν - 1) (n - 1) : ℝ)) *
          Real.cos θ ^ ν * Real.sin ((ν : ℝ) * θ) =
      (2 : ℝ) ^ (n + k) * Real.cos θ ^ (n + k) *
        Real.sin (((n : ℝ) - (k : ℝ)) * θ)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Lemma 3.

TheoremGould's reciprocal binomial identity (Alzer–Kwong, Lemma 4)#●ready to prove

Let \(N\) be a natural number and \(x\) a real number with \(x \ne \nu\) for every \(\nu \in \{0, 1, \dots, N\}\). Then

\[ \sum_{\nu=0}^{N} \frac{(-1)^\nu}{x - \nu} \binom{N}{\nu} = \frac{(-1)^N}{(x - N) \binom{x}{N}}, \]

where \(\binom{x}{N} = x(x-1)\cdots(x-N+1)/N!\) is the generalized binomial coefficient.

theorem_wanted sum_neg_one_pow_div_mul_choose_eq
    (N : ℕ) (x : ℝ)
    (hx : ∀ ν ∈ Finset.Icc 0 N, x ≠ (ν : ℝ)) :
    ∑ ν ∈ Finset.Icc 0 N,
        ((-1 : ℝ) ^ ν / (x - (ν : ℝ))) *
          (Nat.choose N ν : ℝ) =
      (-1 : ℝ) ^ N / ((x - (N : ℝ)) * Ring.choose x N)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Lemma 4.

TheoremUniqueness of the harmonic solution of the diagonal Ramanujan identity#●ready to prove

Let \(K : \mathbb{N} \to \mathbb{C}\) be a sequence such that for every integer \(n \ge 2\)

\[ \sum_{\nu=2}^{n} \Bigl(\binom{2n-\nu-2}{n-1} - \binom{2n-\nu-2}{n-2}\Bigr) K(\nu) = \binom{2n-1}{n-1} \bigl(K(n-1) - K(n)\bigr). \]

Then there is a constant \(\lambda \in \mathbb{C}\) such that \(K(r) = \lambda H_r\) for every integer \(r \ge 1\), where \(H_r = \sum_{j=1}^{r} 1/j\) is the \(r\)-th harmonic number.

theorem_wanted eq_lambda_mul_harmonic_of_sum_choose_sub_mul_eq
    (K : ℕ → ℂ)
    (hK : ∀ n : ℕ, 2 ≤ n →
      ∑ ν ∈ Finset.Icc 2 n,
          (((Nat.choose (2 * n - ν - 2) (n - 1) : ℂ) -
            (Nat.choose (2 * n - ν - 2) (n - 2) : ℂ)) * K ν) =
        (Nat.choose (2 * n - 1) (n - 1) : ℂ) * (K (n - 1) - K n)) :
    ∃ lam : ℂ, ∀ r : ℕ, 1 ≤ r → K r = lam * (harmonic r : ℂ)

Sources

• Horst Alzer and Man Kam Kwong, "Ramanujan and a Combinatorial Identity Involving Harmonic Numbers", Theorem 8.

6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.