Integrals of cosⁿx sin nx

TheoremRamanujan's integrals of \(\cos^n x \sin nx\) for every \(n \ge 0\)#✓fully proved

Let \(n\) be a natural number and let \(H_n = \sum_{k=1}^{n} 1/k\) be the \(n\)-th harmonic number. Then \(x \cos^n x \sin(nx)\) and \(\cos^n x \sin(nx)\) are integrable on \([0, \pi/2]\), \(\int_0^{\pi/2} x \cos^n x \sin(nx)\,dx = \frac{\pi}{2^{n+2}} H_n\) and \(\int_0^{\pi/2} \cos^n x \sin(nx)\,dx = \frac{1}{2^{n+1}} \sum_{k=1}^{n} \frac{2^k}{k}\).

This is Entry 33 without the hypothesis \(n > 0\): at \(n = 0\) both sides of each identity are \(0\).

theorem ramanujan_part1_ch9_entry33_zeta3integral_general (n : ℕ) :
    IntervalIntegrable (chapter9Entry33WeightedIntegrand n) volume 0
        (Real.pi / 2) ∧
      IntervalIntegrable (chapter9Entry33Integrand n) volume 0
        (Real.pi / 2) ∧
      (∫ x in (0 : ℝ)..Real.pi / 2,
          chapter9Entry33WeightedIntegrand n x) =
        Real.pi / (2 : ℝ) ^ (n + 2) * ((harmonic n : ℚ) : ℝ) ∧
      (∫ x in (0 : ℝ)..Real.pi / 2, chapter9Entry33Integrand n x) =
        1 / (2 : ℝ) ^ (n + 1) *
          ∑ k ∈ Icc 1 n, (2 : ℝ) ^ k / (k : ℝ)

Used by 1

Used byRamanujan's integrals of \(\cos^n x \sin nx\) (Entry 33)

TheoremRamanujan's integrals of \(\cos^n x \sin nx\) (Entry 33)#✓fully proved

Let \(n\) be a positive integer and let \(H_n = \sum_{k=1}^{n} 1/k\) be the \(n\)-th harmonic number. Then \(x \cos^n x \sin(nx)\) and \(\cos^n x \sin(nx)\) are integrable on \([0, \pi/2]\), \(\int_0^{\pi/2} x \cos^n x \sin(nx)\,dx = \frac{\pi}{2^{n+2}} H_n\) and \(\int_0^{\pi/2} \cos^n x \sin(nx)\,dx = \frac{1}{2^{n+1}} \sum_{k=1}^{n} \frac{2^k}{k}\).

theorem ramanujan_part1_ch9_entry33_zeta3integral (n : ℕ) (hn : 0 < n) :
    IntervalIntegrable (chapter9Entry33WeightedIntegrand n) volume 0
        (Real.pi / 2) ∧
      IntervalIntegrable (chapter9Entry33Integrand n) volume 0
        (Real.pi / 2) ∧
      (∫ x in (0 : ℝ)..Real.pi / 2,
          chapter9Entry33WeightedIntegrand n x) =
        Real.pi / (2 : ℝ) ^ (n + 2) * ((harmonic n : ℚ) : ℝ) ∧
      (∫ x in (0 : ℝ)..Real.pi / 2, chapter9Entry33Integrand n x) =
        1 / (2 : ℝ) ^ (n + 1) *
          ∑ k ∈ Icc 1 n, (2 : ℝ) ^ k / (k : ℝ)

Sources

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

Uses 1

Proof usesRamanujan's integrals of \(\cos^n x \sin nx\) for every \(n \ge 0\)

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.