Arctangent sums and series

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

For every natural number \(n\),

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

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

theorem ramanujan_part1_ch2_entry3_general (n : ℕ) :
    ∑ k ∈ Finset.Icc 1 (2 * n + 1), Real.arctan (1 / ((↑n + ↑k : ℝ))) =
      Real.pi / 4 + ∑ k ∈ Finset.Icc 1 n,
          Real.arctan ((10 * (↑k : ℝ)) / ((3 * (↑k : ℝ) ^ 2 + 2) * (9 * (↑k : ℝ) ^ 2 - 1)))
Used by 2
Used byRamanujan's arctangent identity for \(\sum_{k=1}^{2n+1} \arctan(1/(n+k))\) · Ramanujan's arctangent series for \(\log 3 - \pi/4\)

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

For every positive integer \(n\),

\[\sum_{k=1}^{2n+1} \arctan \frac{1}{n+k} = \frac{\pi}{4} + \sum_{k=1}^{n} \arctan \frac{10k}{(3k^2 + 2)(9k^2 - 1)}.\]
theorem ramanujan_part1_ch2_entry3 (n : ℕ) (hn : 0 < n) :
    ∑ k ∈ Finset.Icc 1 (2 * n + 1), Real.arctan (1 / ((↑n + ↑k : ℝ))) =
      Real.pi / 4 + ∑ k ∈ Finset.Icc 1 n,
          Real.arctan ((10 * (↑k : ℝ)) / ((3 * (↑k : ℝ) ^ 2 + 2) * (9 * (↑k : ℝ) ^ 2 - 1)))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 3, formula (3.1), printed p. 27 / PDF p. 37.
Uses 1
Proof usesRamanujan's arctangent identity for \(\sum_{k=1}^{2n+1} \arctan(1/(n+k))\), \(n \ge 0\)

TheoremRamanujan's arctangent series for \(\log 3 - \pi/4\)#✓fully proved

The series

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

converges, and its sum is \(\log 3 - \pi/4\).

theorem ramanujan_part1_ch2_entry3_infinite_evaluation :
    HasSum (fun n : ℕ =>
        Real.arctan (10 * ((n : ℝ) + 1) /
            ((3 * ((n : ℝ) + 1) ^ 2 + 2) * (9 * ((n : ℝ) + 1) ^ 2 - 1))))
                (Real.log 3 - Real.pi / 4)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, consequence following Entry 3, printed p. 28 / PDF p. 38.
Uses 1
Proof usesRamanujan's arctangent identity for \(\sum_{k=1}^{2n+1} \arctan(1/(n+k))\), \(n \ge 0\)

TheoremRamanujan's finite arctangent sum (Entry 7)#✓fully proved

For every real number \(n > 0\) and every natural number \(r\),

\[\sum_{k=0}^{r-1} \arctan \frac{2}{(n + 2k + 1)^2} = \arctan \frac{2r}{n^2 + 2nr + 1}.\]
theorem ramanujan_part1_ch2_entry7 (n : ℝ) (r : ℕ) (hn : 0 < n) :
    ∑ k ∈ Finset.range r, Real.arctan (2 / (n + 2 * (k : ℝ) + 1) ^ 2) =
      Real.arctan (2 * (r : ℝ) / (n ^ 2 + 2 * n * (r : ℝ) + 1))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, formula (7.2), printed pp. 35-36 / PDF pp. 45-46.
Used by 4
Used byRamanujan's infinite arctangent series (corollary to Entry 7) · Arctangent series with halved squares (Entry 7, Example 3) · Series of arctangents of 1/(2k²) (Entry 7, Example 5) · Series of arctangents of 1/(1 + k√2)² (Entry 7, Example 6)

TheoremRamanujan's infinite arctangent series (corollary to Entry 7)#✓fully proved

For every real number \(n > 0\), the series

\[\sum_{k=0}^{\infty} \arctan \frac{2}{(n + 2k + 1)^2}\]

converges absolutely and its sum is \(\arctan(1/n)\).

theorem ramanujan_part1_ch2_entry7_corollary (n : ℝ) (hn : 0 < n) :
    HasSum (fun k : ℕ => Real.arctan (2 / ((n + 2 * (k : ℝ) + 1) ^ 2))) (Real.arctan (1 / n))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, corollary to Entry 7, formula (7.3), printed p. 36 / PDF p. 46.
Uses 1
Proof usesRamanujan's finite arctangent sum (Entry 7)

TheoremArctangent series over consecutive shifts (Entry 7, Example 1)#✓fully proved

Let \(n > 0\) be a real number with \(n \ne (\sqrt{5} - 1)/2\). Then the series

\[\sum_{k=0}^{\infty} \arctan \frac{2}{(n + k + 1)^2}\]

converges absolutely; its sum is \(\arctan \frac{2n + 1}{n^2 + n - 1}\) when \(n > (\sqrt{5} - 1)/2\), and \(\arctan \frac{2n + 1}{n^2 + n - 1} + \pi\) when \(n < (\sqrt{5} - 1)/2\). Here \(\arctan\) is the principal branch, with values in \((-\pi/2, \pi/2)\).

theorem ramanujan_part1_ch2_entry7_example1 (n : ℝ)
    (hn_pos : 0 < n) (hn_ne : n ≠ (Real.sqrt 5 - 1) / 2) :
    HasSum (fun k : ℕ => Real.arctan (2 / ((n + (k : ℝ) + 1) ^ 2)))
      (Real.arctan ((2 * n + 1) / (n ^ 2 + n - 1)) + if n < (Real.sqrt 5 - 1) / 2 then Real.pi else
          0)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 1, formula (7.4), printed p. 36 / PDF p. 46.

TheoremArctangent series at the exceptional point (Entry 7, Example 1)#✓fully proved

Let \(c = (\sqrt{5} - 1)/2\). The series

\[\sum_{k=0}^{\infty} \arctan \frac{2}{(c + k + 1)^2}\]

converges absolutely and its sum is \(\pi/2\).

theorem ramanujan_part1_ch2_entry7_example1_boundary :
    HasSum (fun k : ℕ => Real.arctan ((2 : ℝ) / (((Real.sqrt 5 - 1) / 2 + ((k : ℝ) + 1)) ^ 2)))
        (Real.pi / 2)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, boundary consequence of Entry 7, Example 1, formula (7.4), printed p. 36 / PDF p. 46.

TheoremAlternating arctangent series (Entry 7, Example 2)#✓fully proved

For every real number \(n > 0\), the series

\[\sum_{k=0}^{\infty} (-1)^k \arctan \frac{2}{(n + k + 1)^2}\]

converges absolutely and its sum is \(\arctan \frac{1}{n^2 + n + 1}\).

theorem ramanujan_part1_ch2_entry7_example2 (n : ℝ) (hn : 0 < n) :
    HasSum (fun k : ℕ => (-1 : ℝ) ^ k * Real.arctan (2 / (n + (k : ℝ) + 1) ^ 2))
        (Real.arctan (1 / (n ^ 2 + n + 1)))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 2, formula (7.5), printed p. 36 / PDF p. 46.

TheoremArctangent series with halved squares (Entry 7, Example 3)#✓fully proved

For every real number \(n > 0\), the series

\[\sum_{k=0}^{\infty} \arctan \frac{1}{2(n + k + 1)^2}\]

converges absolutely and its sum is \(\arctan \frac{1}{2n + 1}\).

theorem ramanujan_part1_ch2_entry7_example3 (n : ℝ) (hn : 0 < n) :
    HasSum (fun k : ℕ => Real.arctan (1 / (2 * (n + (k : ℝ) + 1) ^ 2)))
      (Real.arctan (1 / (2 * n + 1)))
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 3, formula (7.6), printed p. 36 / PDF p. 46.
Uses 1
Proof usesRamanujan's finite arctangent sum (Entry 7)

TheoremSeries of arctangents of 2/k² (Entry 7, Example 4)#✓fully proved

The series

\[\sum_{k=0}^{\infty} \arctan \frac{2}{(k + 1)^2}\]

converges absolutely and its sum is \(3\pi/4\).

theorem ramanujan_part1_ch2_entry7_example4 :
    HasSum (fun k : ℕ => Real.arctan (2 / (((k : ℝ) + 1) ^ 2))) (3 * Real.pi / 4)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 4, printed p. 37 / PDF p. 47.

TheoremAlternating series of arctangents of 2/k² (Entry 7, Example 5)#✓fully proved

The series

\[\sum_{n=0}^{\infty} (-1)^n \arctan \frac{2}{(n + 1)^2}\]

converges absolutely and its sum is \(\pi/4\).

theorem ramanujan_part1_ch2_entry7_example5_alternating :
    HasSum (fun n : ℕ => (-1 : ℝ) ^ n * Real.arctan ((2 : ℝ) / (((n : ℝ) + 1) ^ 2))) (Real.pi / 4)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 5, printed p. 37 / PDF p. 47.

TheoremSeries of arctangents of 1/(2k²) (Entry 7, Example 5)#✓fully proved

The series

\[\sum_{n=0}^{\infty} \arctan \frac{1}{2(n + 1)^2}\]

converges absolutely and its sum is \(\pi/4\).

theorem ramanujan_part1_ch2_entry7_example5_first :
    HasSum (fun n : ℕ => Real.arctan (1 / (2 * ((n + 1 : ℕ) : ℝ) ^ 2))) (Real.pi / 4)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 5, printed p. 37 / PDF p. 47.
Uses 1
Proof usesRamanujan's finite arctangent sum (Entry 7)

TheoremSeries of arctangents of 1/(1 + k√2)² (Entry 7, Example 6)#✓fully proved

The series

\[\sum_{k=0}^{\infty} \arctan \frac{1}{\bigl(1 + \sqrt{2}\,(k + 1)\bigr)^2}\]

converges absolutely and its sum is \(\pi/8\).

theorem ramanujan_part1_ch2_entry7_example6 :
    HasSum (fun k : ℕ => Real.arctan (1 / ((1 + Real.sqrt 2 * (↑(k + 1) : ℝ)) ^ 2)))
      (Real.pi / 8)
Sources
  • Bruce C. Berndt, Ramanujan's Notebooks, Part I (Springer, 1985), Chapter 2, Entry 7, Example 6, printed p. 37 / PDF p. 47. It follows from Entry7.ramanujan_part1_ch2_entry7 at n = 1 + √2, whose partial sums arctan (2 r / (n ^ 2 + 2 n r + 1)) tend to arctan (1 / n) = arctan (√2 - 1) = π / 8.
Uses 1
Proof usesRamanujan's finite arctangent sum (Entry 7)
13 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.