Ramanujan's harmonic sum identities

TheoremRamanujan's identity for \(\sum_{k=1}^{n} 1/(n+k)\), including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[\sum_{k=1}^{n} \frac{1}{n+k} = \frac{n}{2n+1} + \sum_{k=1}^{n} \frac{1}{(2k)^3 - 2k}.\]

This is Ramanujan's Entry 1 of Chapter 2 without the hypothesis \(n \ge 1\); at \(n = 0\) both sides are \(0\).

theorem ramanujan_part1_ch2_entry1_general (n : ℕ) :
    ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ)) =
      (n : ℝ) / (2 * (n : ℝ) + 1) + ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) /
          ((2 * (k : ℝ)) ^ 3 - 2 * (k : ℝ))

Used by 1

Used byRamanujan's identity for \(\sum_{k=1}^{n} 1/(n+k)\)

TheoremRamanujan's identity for \(\sum_{k=1}^{n} 1/(n+k)\)#✓fully proved

For every positive integer \(n\),

\[\sum_{k=1}^{n} \frac{1}{n+k} = \frac{n}{2n+1} + \sum_{k=1}^{n} \frac{1}{(2k)^3 - 2k}.\]

theorem ramanujan_part1_ch2_entry1 (n : ℕ) (hn : 0 < n) :
    ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ)) =
      (n : ℝ) / (2 * (n : ℝ) + 1) + ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) /
          ((2 * (k : ℝ)) ^ 3 - 2 * (k : ℝ))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 1, formula (1.1), printed p. 25 / PDF p. 35.

Uses 1

Proof usesRamanujan's identity for \(\sum_{k=1}^{n} 1/(n+k)\), including \(n = 0\)

TheoremRamanujan's series \(\sum_{k \ge 1} 1/((2k)^3 - 2k) = \log 2 - 1/2\)#✓fully proved

The series

\[\sum_{k=1}^{\infty} \frac{1}{(2k)^3 - 2k}\]

converges, and its sum is \(\log 2 - \frac{1}{2}\).

theorem ramanujan_part1_ch2_entry1_corollary :
    HasSum (fun n : ℕ => (1 : ℝ) / ((2 * (↑(n + 1) : ℝ)) ^ 3 - 2 * (↑(n + 1) : ℝ)))
        (Real.log 2 - 1 / 2)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 1, printed p. 26 / PDF p. 36.

TheoremRamanujan's identity for \(\sum_{k=1}^{2n+1} 1/(n+k)\), including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[\sum_{k=1}^{2n+1} \frac{1}{n+k} = 1 + 2 \sum_{k=1}^{n} \frac{1}{(3k)^3 - 3k}.\]

This is Ramanujan's Entry 2 of Chapter 2 without the hypothesis \(n \ge 1\); at \(n = 0\) both sides are \(1\).

theorem ramanujan_part1_ch2_entry2_general (n : ℕ) :
    (∑ k ∈ Finset.Icc 1 (2 * n + 1), (1 : ℝ) / ((n : ℝ) + (k : ℝ))) =
    1 + 2 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((3 * (k : ℝ)) ^ 3 - 3 * (k : ℝ))

Used by 1

Used byRamanujan's identity for \(\sum_{k=1}^{2n+1} 1/(n+k)\)

TheoremRamanujan's identity for \(\sum_{k=1}^{2n+1} 1/(n+k)\)#✓fully proved

For every positive integer \(n\),

\[\sum_{k=1}^{2n+1} \frac{1}{n+k} = 1 + 2 \sum_{k=1}^{n} \frac{1}{(3k)^3 - 3k}.\]

theorem ramanujan_part1_ch2_entry2 (n : ℕ) (hn : 0 < n) :
    (∑ k ∈ Finset.Icc 1 (2 * n + 1), (1 : ℝ) / ((n : ℝ) + (k : ℝ))) =
    1 + 2 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((3 * (k : ℝ)) ^ 3 - 3 * (k : ℝ))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 2, formula (2.1), printed p. 27 / PDF p. 37.

Uses 1

Proof usesRamanujan's identity for \(\sum_{k=1}^{2n+1} 1/(n+k)\), including \(n = 0\)

TheoremRamanujan's series \(\sum_{k \ge 1} 1/((3k)^3 - 3k) = (\log 3 - 1)/2\)#✓fully proved

The series

\[\sum_{k=1}^{\infty} \frac{1}{(3k)^3 - 3k}\]

converges, and its sum is \(\frac{\log 3 - 1}{2}\).

theorem ramanujan_part1_ch2_entry2_corollary :
    HasSum (fun j : ℕ => (1 : ℝ) / ((3 * ((j : ℝ) + 1)) ^ 3 - 3 * ((j : ℝ) + 1)))
        ((Real.log 3 - 1) / 2)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 2, printed p. 27 / PDF p. 37.

TheoremRamanujan's sum identity for \(1/((4k)^3 - 4k)\), including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[ \sum_{k=1}^{n} \frac{1}{n+k} + \sum_{k=0}^{n} \frac{1}{2n+2k+1} = 1 + 2 \sum_{k=1}^{n} \frac{1}{(4k)^3 - 4k}. \]

At \(n = 0\) both sides equal \(1\).

theorem ramanujan_part1_ch2_entry4_general (n : ℕ) :
    (∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ))) + (∑ k ∈ Finset.Icc 0 n, (1 : ℝ) /
        (2 * (n : ℝ) + 2 * (k : ℝ) + 1)) =
        1 + 2 * (∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((4 * (k : ℝ)) ^ 3 - 4 * (k : ℝ)))

Used by 1

Used byRamanujan's sum identity for \(1/((4k)^3 - 4k)\)

TheoremRamanujan's sum identity for \(1/((4k)^3 - 4k)\)#✓fully proved

For every positive integer \(n\),

\[ \sum_{k=1}^{n} \frac{1}{n+k} + \sum_{k=0}^{n} \frac{1}{2n+2k+1} = 1 + 2 \sum_{k=1}^{n} \frac{1}{(4k)^3 - 4k}. \]

theorem ramanujan_part1_ch2_entry4 (n : ℕ) (hn : 0 < n) :
    (∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ))) + (∑ k ∈ Finset.Icc 0 n, (1 : ℝ) /
        (2 * (n : ℝ) + 2 * (k : ℝ) + 1)) =
        1 + 2 * (∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((4 * (k : ℝ)) ^ 3 - 4 * (k : ℝ)))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 4, formula (4.1), printed p. 28 / PDF p. 38. It follows from ramanujan_part1_ch2_entry4_general, which extends it to n = 0; the hypothesis hn is unused and keeps the source's shape.

Uses 1

Proof usesRamanujan's sum identity for \(1/((4k)^3 - 4k)\), including \(n = 0\)

TheoremAlternating form of Ramanujan's identity for \(1/((4k)^3 - 4k)\), including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[ 1 + 2 \sum_{k=1}^{n} \frac{1}{(4k)^3 - 4k} = \sum_{k=1}^{4n+1} \frac{(-1)^{k+1}}{k} + \frac{1}{2} \sum_{k=1}^{2n} \frac{(-1)^{k+1}}{k}. \]

theorem ramanujan_part1_ch2_entry4_alternating_form_general (n : ℕ) :
    (1 : ℝ) + 2 * ∑ k ∈ Finset.Icc 1 n, (1 / ((4 * (k : ℝ)) ^ 3 - 4 * (k : ℝ))) =
    (∑ k ∈ Finset.Icc 1 (4 * n + 1), ((-1 : ℝ) ^ (k + 1) / (k : ℝ))) +
    (1 / 2 : ℝ) * ∑ k ∈ Finset.Icc 1 (2 * n), ((-1 : ℝ) ^ (k + 1) / (k : ℝ))

Used by 1

Used byAlternating form of Ramanujan's sum identity for \(1/((4k)^3 - 4k)\)

TheoremAlternating form of Ramanujan's sum identity for \(1/((4k)^3 - 4k)\)#✓fully proved

For every positive integer \(n\),

\[ 1 + 2 \sum_{k=1}^{n} \frac{1}{(4k)^3 - 4k} = \sum_{k=1}^{4n+1} \frac{(-1)^{k+1}}{k} + \frac{1}{2} \sum_{k=1}^{2n} \frac{(-1)^{k+1}}{k}. \]

theorem ramanujan_part1_ch2_entry4_alternating_form (n : ℕ) (hn : 0 < n) :
    (1 : ℝ) + 2 * ∑ k ∈ Finset.Icc 1 n, (1 / ((4 * (k : ℝ)) ^ 3 - 4 * (k : ℝ))) =
    (∑ k ∈ Finset.Icc 1 (4 * n + 1), ((-1 : ℝ) ^ (k + 1) / (k : ℝ))) +
    (1 / 2 : ℝ) * ∑ k ∈ Finset.Icc 1 (2 * n), ((-1 : ℝ) ^ (k + 1) / (k : ℝ))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 4, formula (4.1), printed p. 28 / PDF p. 38.

Uses 1

Proof usesAlternating form of Ramanujan's identity for \(1/((4k)^3 - 4k)\), including \(n = 0\)

TheoremRamanujan's series for \(\frac{3}{2}\log 2 - 1\)#✓fully proved

The numbers \(\frac{2}{(4k)^3 - 4k}\) for \(k = 1, 2, 3, \dots\) are summable with sum \(\frac{3}{2}\log 2 - 1\), where \(\log\) is the natural logarithm.

theorem ramanujan_part1_ch2_entry4_corollary :
    HasSum (fun j : ℕ => (2 : ℝ) / ((4 * ((j : ℝ) + 1)) ^ 3 - 4 * ((j : ℝ) + 1)))
        ((3 : ℝ) / 2 * Real.log 2 - 1)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 4, printed p. 29 / PDF p. 39.

TheoremRamanujan's sum identity for \(1/((6k)^3 - 6k)\), including \(n = 0\)#✓fully proved

For every natural number \(n\),

\[ 1 + 2 \sum_{k=1}^{n} \frac{1}{(6k)^3 - 6k} = \frac{2}{3} \sum_{k=1}^{n} \frac{1}{n+k} + \sum_{k=0}^{2n} \frac{1}{2n+2k+1}. \]

theorem ramanujan_part1_ch2_entry5_general (n : ℕ) :
    (1 : ℝ) + 2 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((6 * (k : ℝ)) ^ 3 - 6 * (k : ℝ)) =
      (2 : ℝ) / 3 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ)) +
        ∑ k ∈ Finset.Icc 0 (2 * n), (1 : ℝ) / (2 * (n : ℝ) + 2 * (k : ℝ) + 1)

Used by 1

Used byRamanujan's sum identity for \(1/((6k)^3 - 6k)\)

TheoremRamanujan's sum identity for \(1/((6k)^3 - 6k)\)#✓fully proved

For every positive integer \(n\),

\[ 1 + 2 \sum_{k=1}^{n} \frac{1}{(6k)^3 - 6k} = \frac{2}{3} \sum_{k=1}^{n} \frac{1}{n+k} + \sum_{k=0}^{2n} \frac{1}{2n+2k+1}. \]

theorem ramanujan_part1_ch2_entry5 (n : ℕ) (hn : 0 < n) :
    (1 : ℝ) + 2 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((6 * (k : ℝ)) ^ 3 - 6 * (k : ℝ)) =
      (2 : ℝ) / 3 * ∑ k ∈ Finset.Icc 1 n, (1 : ℝ) / ((n : ℝ) + (k : ℝ)) +
        ∑ k ∈ Finset.Icc 0 (2 * n), (1 : ℝ) / (2 * (n : ℝ) + 2 * (k : ℝ) + 1)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 5, formula (5.1), printed p. 29 / PDF p. 39.

Uses 1

Proof usesRamanujan's sum identity for \(1/((6k)^3 - 6k)\), including \(n = 0\)

TheoremRamanujan's series for \(\frac{1}{2}\log 3 + \frac{1}{3}\log 4 - 1\)#✓fully proved

The numbers \(\frac{2}{(6k)^3 - 6k}\) for \(k = 1, 2, 3, \dots\) are summable with sum \(\frac{1}{2}\log 3 + \frac{1}{3}\log 4 - 1\), where \(\log\) is the natural logarithm.

theorem ramanujan_part1_ch2_entry5_corollary :
    HasSum (fun j : ℕ => (2 : ℝ) / ((6 * (↑j + 1)) ^ 3 - 6 * (↑j + 1)))
        (1 / 2 * Real.log 3 + 1 / 3 * Real.log 4 - 1)

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 5, printed p. 30 / PDF p. 40.

DefinitionThe tripling sequence of Ramanujan's Entry 6#✓fully proved

For natural numbers \(n\) and \(k\), let \(A(n, k) = 3^k n + (3^k - 1)/2\), a natural number. It is the sequence with \(A(n, 0) = n\) and \(A(n, k + 1) = 3A(n, k) + 1\).

def A (n k : ℕ) : ℕ := 3 ^ k * n + (3 ^ k - 1) / 2

Used by 5

Used byThe tripling sequence never drops below its starting value · Recurrence of the tripling sequence · Starting value of the tripling sequence · Ramanujan's harmonic sum identity (Entry 6) · Ramanujan's harmonic sum identity (Entry 6, general form)

TheoremStarting value of the tripling sequence#✓fully proved

For every natural number \(n\), the tripling sequence \(A(n, k)\) of Entry 6 satisfies \(A(n, 0) = n\).

@[simp]
theorem A_zero (n : ℕ) : A n 0 = n

Uses 1 · Used by 2

Statement usesThe tripling sequence of Ramanujan's Entry 6

Used byThe tripling sequence never drops below its starting value · Ramanujan's harmonic sum identity (Entry 6, general form)

TheoremRecurrence of the tripling sequence#✓fully proved

For all natural numbers \(n\) and \(k\), the tripling sequence \(A(n, k)\) of Entry 6 satisfies \(A(n, k + 1) = 3A(n, k) + 1\).

theorem A_succ (n k : ℕ) : A n (k + 1) = 3 * A n k + 1

Uses 1 · Used by 2

Statement usesThe tripling sequence of Ramanujan's Entry 6

Used byThe tripling sequence never drops below its starting value · Ramanujan's harmonic sum identity (Entry 6, general form)

TheoremThe tripling sequence never drops below its starting value#✓fully proved

For all natural numbers \(n\) and \(k\), the tripling sequence \(A(n, k)\) of Entry 6 satisfies \(n \le A(n, k)\).

theorem A_ge (n k : ℕ) : n ≤ A n k

Uses 3 · Used by 1

Statement usesThe tripling sequence of Ramanujan's Entry 6

Proof usesRecurrence of the tripling sequence · Starting value of the tripling sequence

Used byRamanujan's harmonic sum identity (Entry 6, general form)

TheoremRamanujan's harmonic sum identity (Entry 6, general form)#✓fully proved

For all natural numbers \(n\) and \(r\), the following identity holds in \(\mathbb{Q}\):

\[ \sum_{j=n+1}^{A(n, r)} \frac{1}{j} = r + 2 \sum_{k=0}^{r-1} (r - k) \sum_{j=a_k}^{A(n, k)} \frac{1}{(3j)^3 - 3j}, \]

where \(A(n, k)\) is the tripling sequence of Entry 6, \(a_0 = 1\) and \(a_k = A(n, k - 1) + 1\) for \(k \ge 1\), and a sum over an empty range is \(0\). For \(r = 0\) both sides are \(0\).

theorem ramanujan_part1_ch2_entry6_general (n r : ℕ) :
    ∑ j ∈ Finset.Icc (n + 1) (A n r), (1 : ℚ) / ((j : ℕ) : ℚ)
    = (r : ℚ) + 2 * ∑ k ∈ Finset.range r, (((r - k : ℕ)) : ℚ) *
        ∑ j ∈ Finset.Icc (if k = 0 then 1 else A n (k - 1) + 1) (A n k),
          (1 : ℚ) / ((3 * ((j : ℕ) : ℚ)) ^ 3 - 3 * ((j : ℕ) : ℚ))

Uses 4 · Used by 1

Statement usesThe tripling sequence of Ramanujan's Entry 6

Proof usesThe tripling sequence never drops below its starting value · Recurrence of the tripling sequence · Starting value of the tripling sequence

Used byRamanujan's harmonic sum identity (Entry 6)

TheoremRamanujan's harmonic sum identity (Entry 6)#✓fully proved

For all natural numbers \(n\) and \(r\) with \(r > 0\), the following identity holds in \(\mathbb{Q}\):

\[ \sum_{j=n+1}^{A(n, r)} \frac{1}{j} = r + 2 \sum_{k=0}^{r-1} (r - k) \sum_{j=a_k}^{A(n, k)} \frac{1}{(3j)^3 - 3j}, \]

where \(A(n, k)\) is the tripling sequence of Entry 6 (with \(A(n, 0) = n\) and \(A(n, k + 1) = 3A(n, k) + 1\)), \(a_0 = 1\) and \(a_k = A(n, k - 1) + 1\) for \(k \ge 1\), and a sum over an empty range is \(0\).

theorem ramanujan_part1_ch2_entry6 (n r : ℕ) (hr : 0 < r) :
    ∑ j ∈ Finset.Icc (n + 1) (A n r), (1 : ℚ) / (j : ℚ) =
      (r : ℚ) + 2 * ∑ k ∈ Finset.range r, ((r - k : ℕ) : ℚ) *
          ∑ j ∈ Finset.Icc (if k = 0 then 1 else A n (k - 1) + 1) (A n k), (1 : ℚ) /
              ((3 * (j : ℚ)) ^ 3 - 3 * (j : ℚ))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 6, printed p. 33 / PDF p. 43. It follows from ramanujan_part1_ch2_entry6_general; the hypothesis hr is unused and keeps the source's shape.

Uses 2

Statement usesThe tripling sequence of Ramanujan's Entry 6

Proof usesRamanujan's harmonic sum identity (Entry 6, general form)

DefinitionThe tripling sequence starting at zero#✓fully proved

For a natural number \(k\), let \(A(k) = (3^k - 1)/2 = 1 + 3 + \cdots + 3^{k-1}\), a natural number with \(A(0) = 0\).

def A (k : ℕ) : ℕ := (3 ^ k - 1) / 2

Used by 3

Used byTwice the tripling sequence plus one is a power of three · Ramanujan's harmonic sum identity (corollary to Entry 6) · Ramanujan's harmonic sum identity (corollary to Entry 6, general form)

TheoremTwice the tripling sequence plus one is a power of three#✓fully proved

For every natural number \(k\), \(2A(k) + 1 = 3^k\), where \(A(k) = (3^k - 1)/2\); in particular the division by \(2\) in the definition of \(A(k)\) is exact.

theorem A_two_mul_add_one (k : ℕ) : 2 * A k + 1 = 3 ^ k

Uses 1 · Used by 1

Statement usesThe tripling sequence starting at zero

Used byRamanujan's harmonic sum identity (corollary to Entry 6, general form)

TheoremRamanujan's harmonic sum identity (corollary to Entry 6, general form)#✓fully proved

For every natural number \(r\), the following identity holds in \(\mathbb{Q}\):

\[ \sum_{j=1}^{A(r)} \frac{1}{j} = r + 2 \sum_{k=1}^{r-1} (r - k) \sum_{j=A(k-1)+1}^{A(k)} \frac{1}{(3j)^3 - 3j}, \]

where \(A(k) = (3^k - 1)/2\) and a sum over an empty range is \(0\). For \(r = 0\) both sides are \(0\).

theorem ramanujan_part1_ch2_entry6_corollary_general (r : ℕ) :
    ∑ j ∈ Finset.Icc 1 (A r), (1 : ℚ) / (j : ℚ) = (r : ℚ) + 2 * ∑ k ∈ Finset.Icc 1 (r - 1),
        ((r - k : ℕ) : ℚ) *
            ∑ j ∈ Finset.Icc (A (k - 1) + 1) (A k), (1 : ℚ) / ((3 * (j : ℚ)) ^ 3 - 3 * (j : ℚ))

Uses 2 · Used by 1

Statement usesThe tripling sequence starting at zero

Proof usesTwice the tripling sequence plus one is a power of three

Used byRamanujan's harmonic sum identity (corollary to Entry 6)

TheoremRamanujan's harmonic sum identity (corollary to Entry 6)#✓fully proved

For every natural number \(r > 0\), the following identity holds in \(\mathbb{Q}\):

\[ \sum_{j=1}^{A(r)} \frac{1}{j} = r + 2 \sum_{k=1}^{r-1} (r - k) \sum_{j=A(k-1)+1}^{A(k)} \frac{1}{(3j)^3 - 3j}, \]

where \(A(k) = (3^k - 1)/2 = 1 + 3 + \cdots + 3^{k-1}\) and a sum over an empty range is \(0\).

theorem ramanujan_part1_ch2_entry6_corollary (r : ℕ) (hr : 0 < r) :
    ∑ j ∈ Finset.Icc 1 (A r), (1 : ℚ) / (j : ℚ) = (r : ℚ) + 2 * ∑ k ∈ Finset.Icc 1 (r - 1),
        ((r - k : ℕ) : ℚ) *
            ∑ j ∈ Finset.Icc (A (k - 1) + 1) (A k), (1 : ℚ) / ((3 * (j : ℚ)) ^ 3 - 3 * (j : ℚ))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 6, printed p. 33 / PDF p. 43.

Uses 2

Statement usesThe tripling sequence starting at zero

Proof usesRamanujan's harmonic sum identity (corollary to Entry 6, general form)

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.