Asymptotic expansions of Lambert series

5 fully proved

Entry10 Centralbinomialfull

TheoremSummability of the Lambert series \(\sum_k 1/(e^{kx}-1)\)#✓fully proved

For every real \(x > 0\), the series \(\sum_{k=1}^{\infty} \frac{1}{e^{kx} - 1}\) is summable.

theorem summable_chapter6Entry14MinusTerm (x : ℝ) (hx : 0 < x) :
    Summable (chapter6Entry14MinusTerm x)

Used by 4

Used byRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Asymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Asymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}+1)\) · Summability of the Lambert series \(\sum_k 1/(e^{kx}+1)\)

TheoremRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\)#✓fully proved

Let \(x > 0\) be real and let \(n \ge 1\) be an integer. Let \(S(x) = \sum_{k=1}^{\infty} \frac{1}{e^{kx} - 1}\), let \(B_m\) be the \(m\)-th Bernoulli number, let \(\gamma\) be the Euler–Mascheroni constant, and let \(C_n(x) = \sum_{k=1}^{n} \frac{B_{2k}^2 \, x^{2k-1}}{2k \, (2k)!}\). Then \(\left| S(x) - \left( \frac{\gamma}{x} - \frac{\log x}{x} + \frac14 - C_n(x) \right) \right| \le \frac{|B_{2n} B_{2n+2}| \, x^{2n}}{(2n)!} \left( \frac{x^2}{4\pi^2} + \frac{\pi^2}{6} \right)\).

theorem chapter6Entry14MinusSum_error_le (x : ℝ) (n : ℕ)
    (hx : 0 < x) (hn : 1 ≤ n) :
    |chapter6Entry14MinusSum x -
        (Real.eulerMascheroniConstant / x - Real.log x / x + 1 / 4 -
          chapter6Entry14MinusCorrection n x)| ≤
      |(bernoulli (2 * n) : ℝ) * (bernoulli (2 * n + 2) : ℝ)| *
        x ^ (2 * n) / ((2 * n).factorial : ℝ) *
        (x ^ 2 / (4 * Real.pi ^ 2) + Real.pi ^ 2 / 6)

Uses 3 · Used by 2

Proof usesSummability of the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Euler–Maclaurin formula · Mittag-Leffler expansion of \(1/(e^u - 1)\)

Used byAsymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Asymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}+1)\)

TheoremAsymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}-1)\)#✓fully proved

Let \(x > 0\) be real and let \(n \ge 1\) be an integer. Let \(B_m\) be the \(m\)-th Bernoulli number, let \(\gamma\) be the Euler–Mascheroni constant, and let \(C_n(x) = \sum_{k=1}^{n} \frac{B_{2k}^2 \, x^{2k-1}}{2k \, (2k)!}\). Then the series \(\sum_{k=1}^{\infty} \frac{1}{e^{kx} - 1}\) is summable, and its sum \(S(x)\) satisfies \(\left| S(x) - \left( \frac{\gamma}{x} - \frac{\log x}{x} + \frac14 - C_n(x) \right) \right| \le \frac{|B_{2n} B_{2n+2}| \, x^{2n}}{(2n)!} \left( \frac{x^2}{4\pi^2} + \frac{\pi^2}{6} \right)\).

The proof applies the Euler–Maclaurin formula to the smooth Mittag-Leffler kernel and bounds the periodic Bernoulli remainder by its Fourier series.

theorem ramanujan_part1_ch6_entry10_centralbinomialfull (x : ℝ) (n : ℕ)
    (hx : 0 < x) (hn : 1 ≤ n) :
    Summable (chapter6Entry14MinusTerm x) ∧
      |chapter6Entry14MinusSum x -
          (Real.eulerMascheroniConstant / x - Real.log x / x + 1 / 4 -
            chapter6Entry14MinusCorrection n x)| ≤
        |(bernoulli (2 * n) : ℝ) * (bernoulli (2 * n + 2) : ℝ)| *
          x ^ (2 * n) / ((2 * n).factorial : ℝ) *
          (x ^ 2 / (4 * Real.pi ^ 2) + Real.pi ^ 2 / 6)

Sources

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

Uses 2

Proof usesRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Summability of the Lambert series \(\sum_k 1/(e^{kx}-1)\)

Entry10 Centralbinomialexpansion

TheoremSummability of the Lambert series \(\sum_k 1/(e^{kx}+1)\)#✓fully proved

For every real \(x > 0\), the series \(\sum_{k=1}^{\infty} \frac{1}{e^{kx} + 1}\) is summable.

theorem summable_chapter6Entry14PlusTerm (x : ℝ) (hx : 0 < x) :
    Summable (chapter6Entry14PlusTerm x)

Uses 1

Proof usesSummability of the Lambert series \(\sum_k 1/(e^{kx}-1)\)

TheoremAsymptotic expansion of the Lambert series \(\sum_k 1/(e^{kx}+1)\)#✓fully proved

Let \(x > 0\) be real and let \(n \ge 1\) be an integer. Let \(B_m\) be the \(m\)-th Bernoulli number and let \(D_n(x) = \sum_{k=1}^{n} \frac{(2^{2k} - 1) \, B_{2k}^2 \, x^{2k-1}}{2k \, (2k)!}\). Then the series \(\sum_{k=1}^{\infty} \frac{1}{e^{kx} + 1}\) is summable, and its sum \(T(x)\) satisfies \(\left| T(x) - \left( \frac{\log 2}{x} - \frac14 + D_n(x) \right) \right| \le \frac{|B_{2n} B_{2n+2}| \, x^{2n}}{(2n)!} \left( \frac{x^2}{4\pi^2} + \frac{\pi^2}{6} + 2^{2n+1} \left( \frac{x^2}{\pi^2} + \frac{\pi^2}{6} \right) \right)\).

The proof writes this series as the series \(\sum_k 1/(e^{kx}-1)\) minus twice the same series at \(2x\), and applies the remainder bound for \(\sum_k 1/(e^{kx}-1)\).

theorem ramanujan_part1_ch6_entry10_centralbinomialexpansion (x : ℝ) (n : ℕ)
    (hx : 0 < x) (hn : 1 ≤ n) :
    Summable (chapter6Entry14PlusTerm x) ∧
      |chapter6Entry14PlusSum x -
          (Real.log 2 / x - 1 / 4 + chapter6Entry14PlusCorrection n x)| ≤
        |(bernoulli (2 * n) : ℝ) * (bernoulli (2 * n + 2) : ℝ)| *
          x ^ (2 * n) / ((2 * n).factorial : ℝ) *
          (x ^ 2 / (4 * Real.pi ^ 2) + Real.pi ^ 2 / 6 +
            (2 : ℝ) ^ (2 * n + 1) *
              (x ^ 2 / Real.pi ^ 2 + Real.pi ^ 2 / 6))

Sources

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

Uses 2

Proof usesRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Summability of the Lambert series \(\sum_k 1/(e^{kx}-1)\)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.