Integrals of 1/(1 + uⁿ)

TheoremRamanujan's closed form for \(\int_0^x du/(1 + u^{10})\) (Chapter 8, Entry 14)#✓fully proved

Put \(a_\pm = \sqrt{6 \pm 2\sqrt5}\) and \(b_\pm = \sqrt{10 \pm 2\sqrt5}\). For every real \(x\) with \(0 \le x < 1\),

\[\int_0^x \frac{du}{1 + u^{10}} = \frac{\arctan x}{5} + \frac{a_+}{20} \arctan \frac{a_+ x}{2(1 - x^2)} + \frac{a_-}{20} \arctan \frac{a_- x}{2(1 - x^2)} + \frac{b_+}{40} \log \frac{1 + b_+ x/2 + x^2}{1 - b_+ x/2 + x^2} + \frac{b_-}{40} \log \frac{1 + b_- x/2 + x^2}{1 - b_- x/2 + x^2}.\]

theorem ramanujan_part1_ch8_entry14_qreflection (x : ℝ) (hx0 : 0 ≤ x) (hx1 : x < 1) :
    chapter8Entry14A 10 x = chapter8Entry14A10Closed x

Sources

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

TheoremRamanujan's closed form for \(\int_0^x du/(1 + u^5)\) (Chapter 8, Entry 14(v))#✓fully proved

Let \(x\) be a real number with \(-1 < x < 4/(\sqrt5 + 1)\), and put \(c_\pm = \sqrt{10 \pm 2\sqrt5}\) and

\[Q(x) = \frac{1 + \tfrac12 x(\sqrt5 - 1) + x^2}{1 - \tfrac12 x(\sqrt5 + 1) + x^2}.\]

Then \(u \mapsto 1/(1 + u^5)\) is integrable on the interval between \(0\) and \(x\), \((1 + x)^5/(1 + x^5) > 0\), \(Q(x) > 0\), \(4 + x(\sqrt5 - 1) \ne 0\), \(4 - x(\sqrt5 + 1) \ne 0\), and

\[\int_0^x \frac{du}{1 + u^5} = \frac{1}{20} \log \frac{(1 + x)^5}{1 + x^5} + \frac{1}{4\sqrt5} \log Q(x) + \frac{c_+}{10} \arctan \frac{c_+ x}{4 + x(\sqrt5 - 1)} + \frac{c_-}{10} \arctan \frac{c_- x}{4 - x(\sqrt5 + 1)}.\]

MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry14VIntegral5.ramanujan_part1_ch8_entry14_v_integral5 · 23 lines

theorem ramanujan_part1_ch8_entry14_v_integral5 (x : ℝ) (hxLower : -1 < x)
    (hxUpper : x < 4 / (Real.sqrt 5 + 1)) :
    IntervalIntegrable (fun u : ℝ => 1 / (1 + u ^ (5 : ℕ))) volume 0 x ∧
      0 < (1 + x) ^ 5 / (1 + x ^ 5) ∧
      0 <
        (1 + (1 / 2 : ℝ) * x * (Real.sqrt 5 - 1) + x ^ 2) /
          (1 - (1 / 2 : ℝ) * x * (Real.sqrt 5 + 1) + x ^ 2) ∧
      4 + x * (Real.sqrt 5 - 1) ≠ 0 ∧
      4 - x * (Real.sqrt 5 + 1) ≠ 0 ∧
      chapter8Entry14A 5 x =
        (1 / 20 : ℝ) * Real.log ((1 + x) ^ 5 / (1 + x ^ 5)) +
          1 / (4 * Real.sqrt 5) *
            Real.log
              ((1 + (1 / 2 : ℝ) * x * (Real.sqrt 5 - 1) + x ^ 2) /
                (1 - (1 / 2 : ℝ) * x * (Real.sqrt 5 + 1) + x ^ 2)) +
          (1 / 10 : ℝ) * Real.sqrt (10 + 2 * Real.sqrt 5) *
            Real.arctan
              (x * Real.sqrt (10 + 2 * Real.sqrt 5) /
                (4 + x * (Real.sqrt 5 - 1))) +
          (1 / 10 : ℝ) * Real.sqrt (10 - 2 * Real.sqrt 5) *
            Real.arctan
              (x * Real.sqrt (10 - 2 * Real.sqrt 5) /
                (4 - x * (Real.sqrt 5 + 1)))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8, Entry 14(v), pp. 189–191.

TheoremRamanujan's closed form for \(\int_0^x du/(1 + u^6)\) (Chapter 8, Entry 14(vi))#✓fully proved

For every real number \(x\), the function \(u \mapsto 1/(1 + u^6)\) is integrable on the interval between \(0\) and \(x\), \(1 + \sqrt3\,x + x^2 > 0\), \(1 - \sqrt3\,x + x^2 > 0\), and

\[\int_0^x \frac{du}{1 + u^6} = \frac12 \arctan x + \frac16 \arctan x^3 + \frac{1}{4\sqrt3} \log \frac{1 + \sqrt3\,x + x^2}{1 - \sqrt3\,x + x^2}.\]

theorem ramanujan_part1_ch8_entry14_vi_integral6 (x : ℝ) :
    IntervalIntegrable (fun u : ℝ => 1 / (1 + u ^ (6 : ℕ))) volume 0 x ∧
      0 < 1 + x * Real.sqrt 3 + x ^ 2 ∧
      0 < 1 - x * Real.sqrt 3 + x ^ 2 ∧
      chapter8Entry14A 6 x =
        (1 / 2 : ℝ) * Real.arctan x +
          (1 / 6 : ℝ) * Real.arctan (x ^ 3) +
          1 / (4 * Real.sqrt 3) *
            Real.log
              ((1 + x * Real.sqrt 3 + x ^ 2) /
                (1 - x * Real.sqrt 3 + x ^ 2))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8, Entry 14(vi), pp. 189–190.

TheoremRamanujan's closed form for \(\int_0^x du/(1 + u^8)\) (Chapter 8, Entry 14(vii))#✓fully proved

Put \(s_\pm = \sqrt{2 \pm \sqrt2}\) and, for real \(x\), \(R_\pm(x) = \frac{1 + s_\pm x + x^2}{1 - s_\pm x + x^2}\). For every real \(x\) with \(|x| < 1\), the function \(u \mapsto 1/(1 + u^8)\) is integrable on the interval between \(0\) and \(x\), \(R_+(x) > 0\), \(R_-(x) > 0\), \(1 - x^2 \ne 0\), and

\[\int_0^x \frac{du}{1 + u^8} = \frac{s_+}{16} \left( \log R_+(x) + 2 \arctan \frac{s_+ x}{1 - x^2} \right) + \frac{s_-}{16} \left( \log R_-(x) + 2 \arctan \frac{s_- x}{1 - x^2} \right).\]

MathlibExt.Analysis.Ramanujan.Part1Ch8.Entry14ViiIntegral8.ramanujan_part1_ch8_entry14_vii_integral8 · 22 lines

theorem ramanujan_part1_ch8_entry14_vii_integral8 (x : ℝ) (hx : |x| < 1) :
    IntervalIntegrable (fun u : ℝ => 1 / (1 + u ^ (8 : ℕ))) volume 0 x ∧
      0 <
        (1 + x * Real.sqrt (2 + Real.sqrt 2) + x ^ 2) /
          (1 - x * Real.sqrt (2 + Real.sqrt 2) + x ^ 2) ∧
      0 <
        (1 + x * Real.sqrt (2 - Real.sqrt 2) + x ^ 2) /
          (1 - x * Real.sqrt (2 - Real.sqrt 2) + x ^ 2) ∧
      1 - x ^ 2 ≠ 0 ∧
      chapter8Entry14A 8 x =
        Real.sqrt (2 + Real.sqrt 2) / 16 *
            (Real.log
                ((1 + x * Real.sqrt (2 + Real.sqrt 2) + x ^ 2) /
                  (1 - x * Real.sqrt (2 + Real.sqrt 2) + x ^ 2)) +
              2 * Real.arctan
                (x * Real.sqrt (2 + Real.sqrt 2) / (1 - x ^ 2))) +
          Real.sqrt (2 - Real.sqrt 2) / 16 *
            (Real.log
                ((1 + x * Real.sqrt (2 - Real.sqrt 2) + x ^ 2) /
                  (1 - x * Real.sqrt (2 - Real.sqrt 2) + x ^ 2)) +
              2 * Real.arctan
                (x * Real.sqrt (2 - Real.sqrt 2) / (1 - x ^ 2)))

Sources

• Bruce C. Berndt, Ramanujan's Notebooks, Part I, Chapter 8, Entry 14(vii), pp. 189–190.

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.