Series with odd harmonic numbers

TheoremRamanujan's series identity with odd harmonic numbers (Entry 34)#✓fully proved

For a natural number \(m\) let \(O_m = \sum_{j=0}^{m-1} 1/(2j+1)\). Let \(x\) be real with \(-1/2 < x < 1\). Then \(1 + x > 0\), \(|x| < 1\) and \(|x/(1+x)| < 1\), the series \(\sum_{k \ge 0} \frac{1}{(2k+1)^2} \left(\frac{x}{1+x}\right)^{k+1}\) and \(\sum_{k \ge 0} \frac{(-1)^k\, 2^{2k} (k!)^2}{(2k+1)!} O_{k+1} x^{k+1}\) converge absolutely, and their sums are equal.

theorem ramanujan_part1_ch9_entry34_zeta3doublesum
    (x : ℝ) (hxLower : -(1 / 2 : ℝ) < x) (hxUpper : x < 1) :
    0 < 1 + x ∧
      |x| < 1 ∧
      |x / (1 + x)| < 1 ∧
      Summable (chapter9Entry34LeftTerm x) ∧
      Summable (chapter9Entry34RightTerm x) ∧
      (∑' k : ℕ, chapter9Entry34LeftTerm x k) =
        ∑' k : ℕ, chapter9Entry34RightTerm x k

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9.

TheoremRamanujan's odd harmonic series identity#✓fully proved

Let \(x\) be a real number with \(|x| < 1\). For \(n \ge 0\) put \(h_n = 1 + \frac{1}{3} + \cdots + \frac{1}{2n+1}\), for real \(y\) let \(F(y) = \sum_{n \ge 0} \frac{h_n}{2n+1} y^{2n+1}\), and let \(\operatorname{Li}_2(x) = \sum_{k \ge 1} \frac{x^k}{k^2}\). Then \(1 - x > 0\), \(2 - x \ne 0\) and \(|x/(2-x)| < 1\); the series defining \(F(x/(2-x))\) and the series defining \(\operatorname{Li}_2(x)\) are both summable; and

\[F\left(\frac{x}{2-x}\right) = \frac{(\log(1-x))^2}{8} + \frac{\operatorname{Li}_2(x)}{2}.\]

theorem ramanujan_part1_ch9_entry8_arcsin (x : ℝ) (hx : |x| < 1) :
    0 < 1 - x ∧
      2 - x ≠ 0 ∧
      |x / (2 - x)| < 1 ∧
      Summable (chapter9Entry8FTerm (x / (2 - x))) ∧
      Summable (chapter9Entry8DilogTerm x) ∧
      chapter9Entry8F (x / (2 - x)) =
        (1 / 8 : ℝ) * Real.log (1 - x) ^ 2 +
          (1 / 2 : ℝ) * chapter9Entry8Dilog x

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9, Entry 8, pp. 249–250.

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.