Clausen functions

TheoremTermwise bound for the Clausen series (Chapter 9, Entry 13)#✓fully proved

For natural numbers \(m\) and \(k\) and a real number \(x\), let \(t_k = \sin((k+1)x)/(k+1)^m\) if \(m\) is even and \(t_k = \cos((k+1)x)/(k+1)^m\) if \(m\) is odd. Then \(\lvert t_k\rvert \le 1/(k+1)^m\).

theorem chapter9ClausenTerm_norm_bound (m : ℕ) (x : ℝ) (k : ℕ) :
    ‖chapter9ClausenTerm m x k‖ ≤ 1 / ((((k + 1 : ℕ)) : ℝ) ^ m)

Used by 2

Used bySummability of the Clausen series (Chapter 9, Entry 13) · Integrals of \(u^n \cot(u/2)\) via Clausen functions (Chapter 9, Entry 13)

TheoremSummability of the Clausen series (Chapter 9, Entry 13)#✓fully proved

For every natural number \(m \ge 2\) and every real \(x\), the series \(\sum_{k \ge 1} \sin(kx)/k^m\) (if \(m\) is even) or \(\sum_{k \ge 1} \cos(kx)/k^m\) (if \(m\) is odd) is summable.

theorem chapter9ClausenTerm_summable_of_two_le (m : ℕ) (x : ℝ) (hm : 2 ≤ m) :
    Summable (chapter9ClausenTerm m x)

Uses 1 · Used by 2

Proof usesTermwise bound for the Clausen series (Chapter 9, Entry 13)

Used byOdd-frequency part of a Clausen series for \(m \ge 2\) · Integrals of \(u^n \cot(u/2)\) via Clausen functions (Chapter 9, Entry 13)

TheoremClausen function of order zero (Chapter 9, Entry 13)#✓fully proved

The Clausen-type functions \(C_m\) of Entry 13 are defined by \(C_1(x) = -\log\lvert 2\sin(x/2)\rvert\) and, for \(m \ge 2\), \(C_m(x) = \sum_{k \ge 1} \sin(kx)/k^m\) for even \(m\) and \(C_m(x) = \sum_{k \ge 1} \cos(kx)/k^m\) for odd \(m\), together with the convention \(C_0 = 0\): for every real \(x\), \(C_0(x) = 0\).

theorem chapter9Clausen_zero (x : ℝ) : chapter9Clausen 0 x = 0

TheoremClausen function of order one (Chapter 9, Entry 13)#✓fully proved

The order-one Clausen-type function \(C_1\) of Entry 13 is the log-sine function: for every real \(x\), \(C_1(x) = -\log\lvert 2\sin(x/2)\rvert\), with the convention \(\log 0 = 0\), so that \(C_1\) vanishes at the integer multiples of \(2\pi\).

theorem chapter9Clausen_one (x : ℝ) :
    chapter9Clausen 1 x = -Real.log |2 * Real.sin (x / 2)|

Used by 1

Used byKachi–Tzermias infinite products for \(\zeta(3)\)

TheoremClausen functions of order at least two as series (Chapter 9, Entry 13)#✓fully proved

Let \(C_m\) be the Clausen-type function of Entry 13, with \(C_0 = 0\) and \(C_1(x) = -\log\lvert 2\sin(x/2)\rvert\). For every natural number \(m \ge 2\) and every real \(x\), \(C_m(x) = \sum_{k \ge 1} \sin(kx)/k^m\) if \(m\) is even and \(C_m(x) = \sum_{k \ge 1} \cos(kx)/k^m\) if \(m\) is odd.

theorem chapter9Clausen_of_two_le (m : ℕ) (x : ℝ) (hm : 2 ≤ m) :
    chapter9Clausen m x = ∑' k : ℕ, chapter9ClausenTerm m x k

Used by 2

Used byOdd-frequency part of a Clausen series for \(m \ge 2\) · Kachi–Tzermias infinite products for \(\zeta(3)\)

TheoremIntegrals of \(u^n \cot(u/2)\) via Clausen functions (Chapter 9, Entry 13)#✓fully proved

For real \(x\) let \(C_1(x) = -\log\lvert 2\sin(x/2)\rvert\) and, for \(m \ge 2\), let \(C_m(x) = \sum_{k \ge 1} \sin(kx)/k^m\) if \(m\) is even and \(C_m(x) = \sum_{k \ge 1} \cos(kx)/k^m\) if \(m\) is odd. Let \(n \ge 1\) be a natural number and \(x\) a nonzero real number with \(\lvert x\rvert < 2\pi\). Then the function \(u \mapsto \frac{u^n}{2}\cot\frac{u}{2}\) is integrable on the interval between \(0\) and \(x\); the partial sums \(\sum_{k=1}^{N} \cos(kx)/k\) converge to \(C_1(x)\) as \(N \to \infty\); for every natural number \(m\) with \(2 \le m \le n + 1\) the series defining \(C_m(x)\) is summable; and, with \(\zeta\) the Riemann zeta function,

\[ \int_0^x \frac{u^n}{2}\cot\frac{u}{2}\,du = \cos\frac{n\pi}{2}\,n!\,\zeta(n+1) - \sum_{j=0}^{n} (-1)^{j(j+1)/2}\,\frac{n!}{(n-j)!}\,x^{n-j}\,C_{j+1}(x). \]

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry13Bernoulligen.ramanujan_part1_ch9_entry13_bernoulligen · 16 lines

theorem ramanujan_part1_ch9_entry13_bernoulligen (n : ℕ) (x : ℝ)
    (hn : 1 ≤ n) (hx0 : x ≠ 0) (hx : |x| < 2 * Real.pi) :
    IntervalIntegrable (chapter9Entry13Integrand n) volume 0 x ∧
      Tendsto
        (fun N : ℕ => ∑ k ∈ range N,
          Real.cos (((k + 1 : ℕ) : ℝ) * x) / ((k + 1 : ℕ) : ℝ))
        atTop (𝓝 (chapter9Clausen 1 x)) ∧
      (∀ m : ℕ, 2 ≤ m → m ≤ n + 1 →
        Summable (chapter9ClausenTerm m x)) ∧
      (∫ u in (0 : ℝ)..x, chapter9Entry13Integrand n u) =
        Real.cos (n * Real.pi / 2) * n.factorial *
            (riemannZeta ((n + 1 : ℕ) : ℂ)).re -
          ∑ j ∈ range (n + 1),
            (-1 : ℝ) ^ (j * (j + 1) / 2) *
              (n.factorial : ℝ) / ((n - j).factorial : ℝ) *
              x ^ (n - j) * chapter9Clausen (j + 1) x

Sources

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

Uses 2 · Used by 2

Proof usesTermwise bound for the Clausen series (Chapter 9, Entry 13) · Summability of the Clausen series (Chapter 9, Entry 13)

Used byEntry 14 of Chapter 9: the integral of \(u^n / (2 \sin u)\) · Kachi–Tzermias infinite products for \(\zeta(3)\)

TheoremBound on the terms of the odd Clausen series#✓fully proved

For integers \(m, k \ge 0\) let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. Then for all integers \(m, k \ge 0\) and every real \(x\),

\[\left| \frac{s_m((2k+1)x)}{(2k+1)^m} \right| \le \frac{1}{(2k+1)^m}.\]

theorem chapter9OddClausenTerm_norm_bound (m : ℕ) (x : ℝ) (k : ℕ) :
    ‖chapter9OddClausenTerm m x k‖ ≤ 1 / (((2 * k + 1 : ℕ) : ℝ) ^ m)

Used by 1

Used bySummability of the odd Clausen series for \(m \ge 2\)

TheoremSummability of the odd Clausen series for \(m \ge 2\)#✓fully proved

Let \(m \ge 2\) be an integer, and let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. Then for every real \(x\) the series \(\sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\) is summable.

theorem chapter9OddClausenTerm_summable_of_two_le (m : ℕ) (x : ℝ) (hm : 2 ≤ m) :
    Summable (chapter9OddClausenTerm m x)

Uses 1 · Used by 1

Proof usesBound on the terms of the odd Clausen series

Used byEntry 14 of Chapter 9: the integral of \(u^n / (2 \sin u)\)

TheoremThe odd Clausen function vanishes at \(m = 0\)#✓fully proved

For an integer \(m \ge 0\) let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. The odd Clausen functions \(O_m\), for integers \(m \ge 0\), are given by \(O_1(x) = -\tfrac{1}{2} \log|\tan(x/2)|\), by \(O_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\) for \(m \ge 2\), and at \(m = 0\) by zero: for every real \(x\), \(O_0(x) = 0\).

theorem chapter9OddClausen_zero (x : ℝ) : chapter9OddClausen 0 x = 0

TheoremThe odd Clausen function at \(m = 1\)#✓fully proved

For an integer \(m \ge 0\) let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. The odd Clausen functions \(O_m\), for integers \(m \ge 0\), are given by \(O_0 = 0\), by \(O_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\) for \(m \ge 2\), and at \(m = 1\) by a closed form: for every real \(x\), \(O_1(x) = -\tfrac{1}{2} \log|\tan(x/2)|\).

theorem chapter9OddClausen_one (x : ℝ) :
    chapter9OddClausen 1 x = -(1 / 2 : ℝ) * Real.log |Real.tan (x / 2)|

TheoremThe odd Clausen function as a series for \(m \ge 2\)#✓fully proved

For an integer \(m \ge 0\) let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. For real \(x\), the odd Clausen function \(O_m(x)\) is \(0\) if \(m = 0\), is \(-\tfrac{1}{2} \log|\tan(x/2)|\) if \(m = 1\), and is otherwise given by a series: for every integer \(m \ge 2\) and every real \(x\), \(O_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\).

theorem chapter9OddClausen_of_two_le (m : ℕ) (x : ℝ) (hm : 2 ≤ m) :
    chapter9OddClausen m x = ∑' k : ℕ, chapter9OddClausenTerm m x k

TheoremOdd-frequency part of a Clausen series for \(m \ge 2\)#✓fully proved

Let \(m \ge 2\) be an integer, and let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd. For real \(x\) write \(C_m(x) = \sum_{k \ge 1} s_m(kx)/k^m\) and \(O_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\). Then for every real \(x\), \(O_m(x) = C_m(x) - 2^{-m} C_m(2x)\).

theorem chapter9OddClausen_eq_clausen_sub_of_two_le (m : ℕ) (x : ℝ) (hm : 2 ≤ m) :
    chapter9OddClausen m x = chapter9Clausen m x -
      (1 / (2 : ℝ) ^ m) * chapter9Clausen m (2 * x)

Uses 2 · Used by 1

Proof usesSummability of the Clausen series (Chapter 9, Entry 13) · Clausen functions of order at least two as series (Chapter 9, Entry 13)

Used byOdd-frequency part of a Clausen function for \(0 < |x| < \pi\)

TheoremOdd-frequency part of a Clausen function for \(0 < |x| < \pi\)#✓fully proved

For real \(x\) let \(C_1(x) = -\log|2 \sin(x/2)|\) and \(O_1(x) = -\tfrac{1}{2} \log|\tan(x/2)|\). For an integer \(m \ge 2\), let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd, and let \(C_m(x) = \sum_{k \ge 1} s_m(kx)/k^m\) and \(O_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\). Then for every integer \(m \ge 1\) and every real \(x\) with \(x \ne 0\) and \(|x| < \pi\), \(O_m(x) = C_m(x) - 2^{-m} C_m(2x)\).

theorem chapter9OddClausen_eq_clausen_sub (m : ℕ) (x : ℝ) (hm : 1 ≤ m)
    (hx0 : x ≠ 0) (hx : |x| < Real.pi) :
    chapter9OddClausen m x = chapter9Clausen m x -
      (1 / (2 : ℝ) ^ m) * chapter9Clausen m (2 * x)

Uses 1 · Used by 1

Proof usesOdd-frequency part of a Clausen series for \(m \ge 2\)

Used byEntry 14 of Chapter 9: the integral of \(u^n / (2 \sin u)\)

TheoremOdd reciprocal power sums in terms of \(\zeta\)#✓fully proved

For every integer \(m \ge 2\),

\[\sum_{k \ge 0} \frac{1}{(2k+1)^m} = \left(1 - \frac{1}{2^m}\right) \operatorname{Re} \zeta(m),\]

where \(\zeta\) is the Riemann zeta function.

theorem chapter9ChiAtOne_eq_zeta (m : ℕ) (hm : 2 ≤ m) :
    chapter9ChiAtOne m =
      (1 - 1 / (2 : ℝ) ^ m) * (riemannZeta (m : ℂ)).re

Used by 1

Used byEntry 14 of Chapter 9: the integral of \(u^n / (2 \sin u)\)

TheoremEntry 14 of Chapter 9: the integral of \(u^n / (2 \sin u)\)#✓fully proved

For an integer \(m \ge 2\) write \(\lambda(m) = \sum_{k \ge 0} (2k+1)^{-m}\). For real \(x\) let \(C_1(x) = -\tfrac{1}{2} \log|\tan(x/2)|\), and for an integer \(m \ge 2\) let \(s_m = \sin\) if \(m\) is even and \(s_m = \cos\) if \(m\) is odd, and let \(C_m(x) = \sum_{k \ge 0} s_m((2k+1)x)/(2k+1)^m\). Let \(n \ge 1\) be an integer and \(x\) a real number with \(x \ne 0\) and \(|x| < \pi\). Then \(u \mapsto u^n / (2 \sin u)\) is integrable on the interval between \(0\) and \(x\); the series defining \(\lambda(n+1)\) is summable; the partial sums \(\sum_{k < N} \cos((2k+1)x)/(2k+1)\) tend to \(C_1(x)\) as \(N \to \infty\); for every integer \(m\) with \(2 \le m \le n+1\) the series defining \(C_m(x)\) is summable; and

\[\int_0^x \frac{u^n}{2 \sin u}\,du = \cos\frac{n\pi}{2}\, n!\, \lambda(n+1) - \sum_{j=0}^{n} (-1)^{j(j+1)/2} \frac{n!}{(n-j)!}\, x^{n-j}\, C_{j+1}(x).\]

The proof subtracts a scaled copy of Entry 13 at \(2x\) from Entry 13 at \(x\) and splits the zeta and Clausen series into even and odd frequencies, following Berndt and Lewin, Polylogarithms and Associated Functions, Chapter 4.

MathlibExt.Analysis.Ramanujan.Part1Ch9.Entry14Xoversin.ramanujan_part1_ch9_entry14_xoversin · 19 lines

theorem ramanujan_part1_ch9_entry14_xoversin (n : ℕ) (x : ℝ)
    (hn : 1 ≤ n) (hx0 : x ≠ 0) (hx : |x| < Real.pi) :
    IntervalIntegrable (chapter9Entry14Integrand n) volume 0 x ∧
      Summable (fun k : ℕ =>
        1 / (((2 * k + 1 : ℕ) : ℝ) ^ (n + 1))) ∧
      Tendsto
        (fun N : ℕ => ∑ k ∈ range N,
          Real.cos (((2 * k + 1 : ℕ) : ℝ) * x) /
            ((2 * k + 1 : ℕ) : ℝ))
        atTop (𝓝 (chapter9OddClausen 1 x)) ∧
      (∀ m : ℕ, 2 ≤ m → m ≤ n + 1 →
        Summable (chapter9OddClausenTerm m x)) ∧
      (∫ u in (0 : ℝ)..x, chapter9Entry14Integrand n u) =
        Real.cos (n * Real.pi / 2) * n.factorial *
            chapter9ChiAtOne (n + 1) -
          ∑ j ∈ range (n + 1),
            (-1 : ℝ) ^ (j * (j + 1) / 2) *
              (n.factorial : ℝ) / ((n - j).factorial : ℝ) *
              x ^ (n - j) * chapter9OddClausen (j + 1) x

Sources

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

Uses 4

Proof usesIntegrals of \(u^n \cot(u/2)\) via Clausen functions (Chapter 9, Entry 13) · Odd reciprocal power sums in terms of \(\zeta\) · Summability of the odd Clausen series for \(m \ge 2\) · Odd-frequency part of a Clausen function for \(0 < |x| < \pi\)

TheoremEntry 15 of Chapter 9: integrals of \(u^n \cot u\) at \(\pi/2 - x\)#✓fully proved

For an integer \(k \ge 0\) and real \(y\) write \(F_k(y) = \int_{\pi/4}^{y} u^k \cot u \, du\). Let \(n \ge 0\) be an integer. Then for every integer \(k\) with \(0 \le k \le n\) and every real \(y\) with \(0 < y < \pi\), the function \(u \mapsto u^k \cot u\) is integrable on the interval between \(\pi/4\) and \(y\); and for every real \(x\) with \(0 < x < \pi/2\),

\[2^n F_n(\pi/2 - x) = \sum_{k=0}^{n} (-1)^k \binom{n}{k} \pi^{n-k} \bigl(F_k(2x) - 2^k F_k(x)\bigr) - \sum_{k=0}^{n} (-1)^k \binom{n}{k} \pi^{n-k} F_k(\pi/2).\]

theorem ramanujan_part1_ch9_entry15_xcot (n : ℕ) :
    (∀ k : ℕ, k ≤ n → ∀ y : ℝ, 0 < y → y < Real.pi →
      IntervalIntegrable
        (fun u : ℝ => u ^ k * (Real.cos u / Real.sin u))
        volume (Real.pi / 4) y) ∧
      ∀ x : ℝ, 0 < x → x < Real.pi / 2 →
        (2 : ℝ) ^ n * chapter9CotPrimitive n (Real.pi / 2 - x) =
          (∑ k ∈ range (n + 1),
            (-1 : ℝ) ^ k * (n.choose k : ℝ) * Real.pi ^ (n - k) *
              (chapter9CotPrimitive k (2 * x) -
                (2 : ℝ) ^ k * chapter9CotPrimitive k x)) -
          ∑ k ∈ range (n + 1),
            (-1 : ℝ) ^ k * (n.choose k : ℝ) * Real.pi ^ (n - k) *
              chapter9CotPrimitive k (Real.pi / 2)

Sources

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

16 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.