Central binomial series in trigonometric arguments

TheoremThe central binomial series in \(\sin x\) and \(x \log|2\sin x|\)#✓fully proved

Let \(x\) be a real number with \(|x| \le \pi/2\), and let \(L(x) = x \log|2\sin x|\) for \(x \ne 0\) and \(L(0) = 0\). Then \(|2\sin x| > 0\) if \(x \ne 0\), the series \(S(x) = \sum_{k=0}^{\infty} \binom{2k}{k} \frac{\sin^{2k+1} x}{2^{2k} (2k+1)^2}\) and \(F(x) = \sum_{k=1}^{\infty} \frac{\sin 2kx}{k^2}\) are both summable, and \(S(x) = L(x) + \frac{1}{2} F(x)\).

theorem ramanujan_part1_ch9_entry16_tan (x : ℝ) (hx : |x| ≤ Real.pi / 2) :
    (x ≠ 0 → 0 < |2 * Real.sin x|) ∧
      Summable (Entry16Tanseries.chapter9CentralSineTerm x) ∧
      Summable (chapter9SineFourierTwoTerm x) ∧
      (∑' k : ℕ, Entry16Tanseries.chapter9CentralSineTerm x k) =
        chapter9Entry16LogTerm x +
          (1 / 2 : ℝ) * ∑' j : ℕ, chapter9SineFourierTwoTerm x j

Sources

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

DefinitionTerms of the cosine-minus-sine central binomial series#✓fully proved

For a real number \(x\) and a natural number \(k\), the \(k\)-th term is \(\binom{2k}{k} \frac{\cos^{2k+1} x - \sin^{2k+1} x}{2^{2k} (2k+1)^2}\).

def chapter9Entry16DifferenceTerm (x : ℝ) (k : ℕ) : ℝ :=
  (Nat.choose (2 * k) k : ℝ) *
      (Real.cos x ^ (2 * k + 1) - Real.sin x ^ (2 * k + 1)) /
    ((2 : ℝ) ^ (2 * k) * (((2 * k + 1 : ℕ) : ℝ) ^ 2))

Sources

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

Used by 2

Used byThe central binomial series in \(\cos x\) minus that in \(\sin x\) · Ramanujan's central-binomial sine series identity (Entry 31)

TheoremThe central binomial series in \(\cos x\) minus that in \(\sin x\)#✓fully proved

Let \(x\) be a real number with \(0 \le x \le \pi/4\), and for real \(y\) let \(S(y) = \sum_{k=0}^{\infty} \binom{2k}{k} \frac{\sin^{2k+1} y}{2^{2k} (2k+1)^2}\). Then \(2\cos x > 0\), the series \(D(x) = \sum_{k=0}^{\infty} \binom{2k}{k} \frac{\cos^{2k+1} x - \sin^{2k+1} x} {2^{2k} (2k+1)^2}\) and the series defining \(S(2x)\) are both summable, and \(D(x) = \frac{\pi}{2} \log(2\cos x) - \frac{1}{2} S(2x)\).

theorem ramanujan_part1_ch9_entry16_tanseries (x : ℝ)
    (hx0 : 0 ≤ x) (hxUpper : x ≤ Real.pi / 4) :
    0 < 2 * Real.cos x ∧
      Summable (chapter9Entry16DifferenceTerm x) ∧
      Summable (chapter9CentralSineTerm (2 * x)) ∧
      (∑' k : ℕ, chapter9Entry16DifferenceTerm x k) =
        Real.pi / 2 * Real.log (2 * Real.cos x) -
          (1 / 2 : ℝ) * ∑' k : ℕ, chapter9CentralSineTerm (2 * x) k

Sources

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

Uses 8 · Used by 1

Statement usesTerms of the cosine-minus-sine central binomial series

Proof usesIntegrated 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

Used byRamanujan's central-binomial sine series identity (Entry 31)

TheoremThe central binomial series in \(\cos x\) plus that in \(\sin x\)#✓fully proved

Let \(x\) be a real number with \(0 \le x \le \pi/4\). Then \(2\cos x > 0\), the series \(C(x) = \sum_{k=0}^{\infty} \binom{2k}{k} \frac{\cos^{2k+1} x + \sin^{2k+1} x} {2^{2k} (2k+1)^2}\) and \(T(x) = \sum_{k=0}^{\infty} (-1)^k \frac{\tan^{2k+1} x}{(2k+1)^2}\) are both summable, and \(C(x) = \frac{\pi}{2} \log(2\cos x) + T(x)\).

theorem ramanujan_part1_ch9_entry19_catalangf (x : ℝ)
    (hx0 : 0 ≤ x) (hx : x ≤ Real.pi / 4) :
    0 < 2 * Real.cos x ∧
      Summable (chapter9Entry19CentralTerm x) ∧
      Summable (chapter9Entry19TanTerm x) ∧
      (∑' k : ℕ, chapter9Entry19CentralTerm x k) =
        Real.pi / 2 * Real.log (2 * Real.cos x) +
          ∑' k : ℕ, chapter9Entry19TanTerm x k

Sources

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

TheoremRamanujan's central-binomial sine series identity (Entry 31)#✓fully proved

For real \(y\) let \(\psi(y) = \sum_{k \ge 0} \binom{2k}{k} \sin^{2k+1}(\pi y) / \bigl(2^{2k} (2k+1)^2\bigr)\). If \(0 \le x \le 1/4\), then the series defining \(\psi(1/2 - x)\), \(\psi(2x)\) and \(\psi(x)\) converge absolutely, \(2 \cos(\pi x) > 0\), and \(\psi(1/2 - x) + \tfrac12 \psi(2x) - \psi(x) = \tfrac{\pi}{2} \log(2 \cos(\pi x))\).

theorem ramanujan_part1_ch9_entry31_ramanujansum
    (x : ℝ) (hxLower : 0 ≤ x) (hxUpper : x ≤ 1 / 4) :
    Summable (chapter9PsiTerm (1 / 2 - x)) ∧
      Summable (chapter9PsiTerm (2 * x)) ∧
      Summable (chapter9PsiTerm x) ∧
      0 < 2 * Real.cos (Real.pi * x) ∧
      (∑' k : ℕ, chapter9PsiTerm (1 / 2 - x) k) +
          (1 / 2 : ℝ) * ∑' k : ℕ, chapter9PsiTerm (2 * x) k -
          ∑' k : ℕ, chapter9PsiTerm x k =
        Real.pi / 2 * Real.log (2 * Real.cos (Real.pi * x))

Sources

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

Uses 2

Proof usesTerms of the cosine-minus-sine central binomial series · The central binomial series in \(\cos x\) minus that in \(\sin x\)

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.