Power series in sin x and tan x

TheoremA series in even powers of \(\sin x\) involving \(\zeta(3)\)#✓fully proved

Let \(x\) be a real number with \(|x| \le \pi/2\), let \(M(x) = \frac{x^2}{2} \log|2\sin x|\) for \(x \ne 0\) and \(M(0) = 0\), and let \(\zeta(3) = \sum_{k=1}^{\infty} k^{-3}\). Then \(|2\sin x| > 0\) if \(x \ne 0\), the series \(\sum_{k=1}^{\infty} k^{-3}\), \(A(x) = \sum_{k=0}^{\infty} \frac{2^{2k} (k!)^2 \sin^{2k+2} x}{(2k+1)! \, (2k+2)^2}\), \(B(x) = \sum_{k=1}^{\infty} \frac{\sin 2kx}{k^2}\) and \(E(x) = \sum_{k=1}^{\infty} \frac{\cos 2kx}{k^3}\) are all summable, and \(A(x) = M(x) + \frac{x}{2} B(x) + \frac{1}{4} E(x) - \frac{\zeta(3)}{4}\).

theorem ramanujan_part1_ch9_entry20_piseries1 (x : ℝ) (hx : |x| ≤ Real.pi / 2) :
    (x ≠ 0 → 0 < |2 * Real.sin x|) ∧
      Summable chapter9ZetaThreeTerm ∧
      Summable (chapter9Entry23FactorialTerm x) ∧
      Summable (chapter9SineFourierTwoTerm x) ∧
      Summable (chapter9CosineFourierThreeTerm x) ∧
      (∑' k : ℕ, chapter9Entry23FactorialTerm x k) =
        chapter9Entry20LogTerm x +
          x / 2 * ∑' j : ℕ, chapter9SineFourierTwoTerm x j +
          (1 / 4 : ℝ) * ∑' j : ℕ, chapter9CosineFourierThreeTerm x j -
          chapter9ZetaThree / 4

Sources

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

Used by 1

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks

TheoremA series in even powers of \(\tan x\) with odd harmonic numbers#✓fully proved

Let \(x\) be a real number with \(|x| \le \pi/4\). Let \(h_k = \sum_{j=0}^{k-1} \frac{1}{2j+1}\), let \(N(x) = \frac{x^2}{2} \log|\tan x|\) for \(x \ne 0\) and \(N(0) = 0\), and let \(\lambda(3) = \sum_{j=0}^{\infty} (2j+1)^{-3}\). Then the series \(\sum_{j=0}^{\infty} (2j+1)^{-3}\), \(A(x) = \sum_{k=1}^{\infty} (-1)^{k-1} \frac{h_k \tan^{2k} x}{(2k)^2}\), \(B(x) = \sum_{j=0}^{\infty} \frac{\sin((4j+2)x)}{(2j+1)^2}\) and \(E(x) = \sum_{j=0}^{\infty} \frac{\cos((4j+2)x)}{(2j+1)^3}\) are all summable, and \(A(x) = N(x) + x B(x) + \frac{1}{2} E(x) - \frac{1}{2} \lambda(3)\).

theorem ramanujan_part1_ch9_entry21_piseries2 (x : ℝ) (hx : |x| ≤ Real.pi / 4) :
    Summable chapter9Chi3Term ∧
      Summable (chapter9Entry21LeftTerm x) ∧
      Summable (chapter9Entry21SineTerm x) ∧
      Summable (chapter9Entry21CosineTerm x) ∧
      (∑' j : ℕ, chapter9Entry21LeftTerm x j) =
        chapter9TanLogTerm x +
          x * ∑' j : ℕ, chapter9Entry21SineTerm x j +
          (1 / 2 : ℝ) * ∑' j : ℕ, chapter9Entry21CosineTerm x j -
          (1 / 2 : ℝ) * chapter9Chi3AtOne

Sources

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

Used by 2

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks · The inverse tangent integral at \(\tan x\)

TheoremOdd reciprocal cubes in Entries 21 and 22#✓fully proved

The sequence \(j \mapsto 1/(2j+1)^3\) (\(j = 0, 1, 2, \dots\)) used in the statement of Entry 22 of Chapter 9 of Ramanujan's notebooks is, by definition, the same sequence as the one used in Entry 21.

theorem chapter9Chi3Term_eq_entry21 :
    chapter9Chi3Term = Entry21Piseries2.chapter9Chi3Term

Used by 1

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks

TheoremThe sum of the odd reciprocal cubes in Entries 21 and 22#✓fully proved

The constant \(\sum_{j \ge 0} 1/(2j+1)^3\) used in the statement of Entry 22 of Chapter 9 of Ramanujan's notebooks is, by definition, the same constant as the one used in Entry 21.

theorem chapter9Chi3AtOne_eq_entry21 :
    chapter9Chi3AtOne = Entry21Piseries2.chapter9Chi3AtOne

Used by 1

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks

TheoremThe factorial sine series term in Entries 20 and 22#✓fully proved

For real \(u\) and \(k \ge 0\), the term \(2^{2k} (k!)^2 \sin^{2k+2} u / \bigl((2k+1)! \, (2k+2)^2\bigr)\) used in the statement of Entry 22 of Chapter 9 of Ramanujan's notebooks is, by definition, the same as the one used in Entry 20.

theorem chapter9Entry23FactorialTerm_eq_entry20 :
    chapter9Entry23FactorialTerm = Entry20Piseries1.chapter9Entry23FactorialTerm

Used by 1

Used byEntry 22 of Chapter 9 of Ramanujan's notebooks

TheoremEntry 22 of Chapter 9 of Ramanujan's notebooks#✓fully proved

For real \(u\) and \(k \ge 0\) let \(T_k(u) = \frac{2^{2k} (k!)^2 \sin^{2k+2} u}{(2k+1)! \, (2k+2)^2}\). Let \(x\) be real with \(0 \le x \le \pi/4\). Then \(2 \cos x > 0\), the series \(\sum_{j \ge 0} \frac{1}{(2j+1)^3}\), \(\sum_{k \ge 0} \bigl(T_k(x) + T_k(\pi/2 - x)\bigr)\), \(\sum_{k \ge 0} \frac{\binom{2k}{k} \cos^{2k+1} x}{2^{2k} (2k+1)^2}\) and \(\sum_{k \ge 0} T_k(2x)\) converge absolutely, and

\[ \sum_{k \ge 0} \bigl(T_k(x) + T_k(\pi/2 - x)\bigr) = -\frac{\pi^2}{8} \log(2 \cos x) + \frac{\pi}{2} \sum_{k \ge 0} \frac{\binom{2k}{k} \cos^{2k+1} x}{2^{2k} (2k+1)^2} + \frac{1}{4} \sum_{k \ge 0} T_k(2x) - \frac{1}{2} \sum_{j \ge 0} \frac{1}{(2j+1)^3}. \]

Proof: Differentiate the factorial and central-binomial series termwise, reduce the logarithmic integral by Abel's limit and dominated convergence, and finish by the fundamental theorem of calculus. This follows Berndt's Entries 20–23 and Lehmer's arcsine series.

theorem ramanujan_part1_ch9_entry22_chudnovsky (x : ℝ)
    (hx0 : 0 ≤ x) (hx : x ≤ Real.pi / 4) :
    0 < 2 * Real.cos x ∧
      Summable chapter9Chi3Term ∧
      Summable (chapter9Entry22LeftTerm x) ∧
      Summable (chapter9Entry22CentralTerm x) ∧
      Summable (chapter9Entry23FactorialTerm (2 * x)) ∧
      (∑' k : ℕ, chapter9Entry22LeftTerm x k) =
        -(Real.pi ^ 2 / 8) * Real.log (2 * Real.cos x) +
          Real.pi / 2 * ∑' k : ℕ, chapter9Entry22CentralTerm x k +
          (1 / 4 : ℝ) *
            ∑' k : ℕ, chapter9Entry23FactorialTerm (2 * x) k -
          (1 / 2 : ℝ) * chapter9Chi3AtOne

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9, Entry 22, pp. 270–271. The printed range 0 ≤ x ≤ π / 2 is false. This target uses 0 ≤ x ≤ π / 4, the range supported by the source proof's substitution of 2 * x into Entry 20; the endpoint remains an explicit proof obligation.

Uses 13

Proof usesA series in even powers of \(\sin x\) involving \(\zeta(3)\) · A series in even powers of \(\tan x\) with odd harmonic numbers · The sum of the odd reciprocal cubes in Entries 21 and 22 · Odd reciprocal cubes in Entries 21 and 22 · The factorial sine series term in Entries 20 and 22 · Integrated arcsine series · Terms of the integrated arcsine series · The integrated arcsine series vanishes at the origin · Normalized central binomial coefficient · Continuity of the integrated arcsine series · Derivative of the integrated arcsine series · Summability of the integrated arcsine series · Lehmer's central binomial series for arcsin

TheoremEntry 23 of Chapter 9 of Ramanujan's notebooks#✓fully proved

For real \(u\) and \(k \ge 0\) let \(T_k(u) = \frac{2^{2k} (k!)^2 \sin^{2k+2} u}{(2k+1)! \, (2k+2)^2}\), and for \(k \ge 1\) let \(O_k = 1 + \frac{1}{3} + \dots + \frac{1}{2k-1}\). Let \(x\) be real with \(|x| \le \pi/4\). Then the series \(\sum_{k \ge 1} \frac{(-1)^{k-1} O_k \tan^{2k} x}{(2k)^2}\), \(\sum_{k \ge 0} T_k(x)\) and \(\sum_{k \ge 0} T_k(2x)\) converge absolutely, and

\[ \sum_{k \ge 1} \frac{(-1)^{k-1} O_k \tan^{2k} x}{(2k)^2} = 2 \sum_{k \ge 0} T_k(x) - \frac{1}{4} \sum_{k \ge 0} T_k(2x). \]

theorem ramanujan_part1_ch9_entry23_ramanujanpi2 (x : ℝ)
    (hx : |x| ≤ Real.pi / 4) :
    Summable (chapter9Entry23LeftTerm x) ∧
      Summable (chapter9Entry23FactorialTerm x) ∧
      Summable (chapter9Entry23FactorialTerm (2 * x)) ∧
      (∑' j : ℕ, chapter9Entry23LeftTerm x j) =
        2 * ∑' k : ℕ, chapter9Entry23FactorialTerm x k -
          (1 / 4 : ℝ) *
            ∑' k : ℕ, chapter9Entry23FactorialTerm (2 * x) k

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 9, Entry 23, p. 271.

TheoremRamanujan's sine series in odd powers of the tangent (Entry 32)#✓fully proved

Let \(x\) be real with \(|x| \le \pi/4\). Then \(\cos x > 0\), the series \(\sum_{k \ge 0} \frac{2^{2k} (k!)^2}{(2k)!\,(2k+1)^2} \sin^{2k+1}(2x)\) and \(\sum_{k \ge 0} \frac{(-1)^k \tan^{2k+1} x}{(2k+1)^2}\) converge absolutely, and the first sum equals twice the second.

theorem ramanujan_part1_ch9_entry32_lambertdivisor (x : ℝ) (hx : |x| ≤ Real.pi / 4) :
    0 < Real.cos x ∧
      Summable (chapter9Entry32LeftTerm x) ∧
      Summable (chapter9Entry19TanTerm x) ∧
      (∑' k : ℕ, chapter9Entry32LeftTerm x k) =
        2 * ∑' k : ℕ, chapter9Entry19TanTerm x k

Sources

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

Used by 1

Used byThe inverse tangent integral at \(\tan x\)

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.