Mittag-Leffler expansion of 1/(e^u − 1)

TheoremMittag-Leffler expansion of \(1/(e^u - 1)\)#✓fully proved

For every real number \(u \neq 0\),

\[ \frac{1}{e^u - 1} = \frac{1}{u} - \frac{1}{2} + \sum_{m=1}^{\infty} \frac{2u}{u^2 + 4\pi^2 m^2}. \]

theorem one_div_exp_sub_one_eq_tsum (u : ℝ) (hu : u ≠ 0) :
    1 / (Real.exp u - 1) = 1 / u - 1 / 2 +
      ∑' m : ℕ, 2 * u / (u ^ 2 + 4 * Real.pi ^ 2 * (m + 1 : ℕ) ^ 2)

Used by 5

Used byRemainder bound for the Lambert series \(\sum_k 1/(e^{kx}-1)\) · Bound on the derivative of the Laurent remainder of \(1/(e^v - 1)\) · Global remainder bound for the Laurent expansion of \(1/(e^v - 1)\) · The Laurent remainder of \(1/(e^v - 1)\) is differentiable · Bound on the Laurent remainder of \(1/(e^v - 1)\)

DefinitionRemainder of the Laurent expansion of \(1/(e^v - 1)\)#✓fully proved

For a natural number \(N\), the function \(R_N : \mathbb{R} \to \mathbb{R}\) is defined by \(R_N(0) = 0\) and, for \(v \neq 0\),

\[ R_N(v) = \frac{1}{e^v - 1} - \frac{1}{v} + \frac{1}{2} - \sum_{n=0}^{N-1} \frac{B_{2n+2}}{(2n+2)!} v^{2n+1}, \]

where \(B_k\) are the Bernoulli numbers. This is the remainder after truncating the Laurent expansion of \(1/(e^v - 1)\) at \(0\) after its first \(N\) terms of positive odd degree.

def oneDivExpSubOneLaurentRemainder (N : ℕ) (v : ℝ) : ℝ :=
  if v = 0 then 0 else
    1 / (Real.exp v - 1) - 1 / v + 1 / 2 -
      ∑ n ∈ Finset.range N,
        (bernoulli (2 * n + 2) : ℝ) / ((2 * n + 2).factorial : ℝ) *
          v ^ (2 * n + 1)

Used by 4

Used byBound on the derivative of the Laurent remainder of \(1/(e^v - 1)\) · The Laurent remainder of \(1/(e^v - 1)\) is differentiable · Bound on the Laurent remainder of \(1/(e^v - 1)\) · Asymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)

TheoremThe Laurent remainder of \(1/(e^v - 1)\) is differentiable#✓fully proved

For every natural number \(N\), the function \(R_N : \mathbb{R} \to \mathbb{R}\) given by \(R_N(0) = 0\) and, for \(v \neq 0\),

\[ R_N(v) = \frac{1}{e^v - 1} - \frac{1}{v} + \frac{1}{2} - \sum_{n=0}^{N-1} \frac{B_{2n+2}}{(2n+2)!} v^{2n+1}, \]

where \(B_k\) are the Bernoulli numbers, is differentiable at every point of \(\mathbb{R}\).

theorem differentiable_oneDivExpSubOneLaurentRemainder (N : ℕ) :
    Differentiable ℝ (oneDivExpSubOneLaurentRemainder N)

Uses 2 · Used by 1

Statement usesRemainder of the Laurent expansion of \(1/(e^v - 1)\)

Proof usesMittag-Leffler expansion of \(1/(e^u - 1)\)

Used byAsymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)

TheoremBound on the Laurent remainder of \(1/(e^v - 1)\)#✓fully proved

For a natural number \(N\), let \(R_N : \mathbb{R} \to \mathbb{R}\) be given by \(R_N(0) = 0\) and, for \(v \neq 0\),

\[ R_N(v) = \frac{1}{e^v - 1} - \frac{1}{v} + \frac{1}{2} - \sum_{n=0}^{N-1} \frac{B_{2n+2}}{(2n+2)!} v^{2n+1}, \]

where \(B_k\) are the Bernoulli numbers. Then for every real number \(v\),

\[ |R_N(v)| \le 2(2N + 3) \left( \sum_{m=0}^{\infty} \frac{1}{(2\pi(m + 1))^{2N+2}} \right) |v|^{2N+1}. \]

theorem oneDivExpSubOneLaurentRemainder_abs_le (N : ℕ) (v : ℝ) :
    |oneDivExpSubOneLaurentRemainder N v| ≤
      (2 * (2 * N + 3 : ℕ) *
        ∑' m : ℕ, ((2 * Real.pi * (m + 1)) ^ (2 * N + 2))⁻¹) *
        |v| ^ (2 * N + 1)

Uses 2 · Used by 1

Statement usesRemainder of the Laurent expansion of \(1/(e^v - 1)\)

Proof usesMittag-Leffler expansion of \(1/(e^u - 1)\)

Used byAsymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)

TheoremBound on the derivative of the Laurent remainder of \(1/(e^v - 1)\)#✓fully proved

For a natural number \(N\), let \(R_N : \mathbb{R} \to \mathbb{R}\) be given by \(R_N(0) = 0\) and, for \(v \neq 0\),

\[ R_N(v) = \frac{1}{e^v - 1} - \frac{1}{v} + \frac{1}{2} - \sum_{n=0}^{N-1} \frac{B_{2n+2}}{(2n+2)!} v^{2n+1}, \]

where \(B_k\) are the Bernoulli numbers. Then for every real number \(v\), the derivative of \(R_N\) satisfies

\[ |R_N'(v)| \le 2(2N + 3) \left( \sum_{m=0}^{\infty} \frac{1}{(2\pi(m + 1))^{2N+2}} \right) |v|^{2N}. \]

theorem abs_deriv_oneDivExpSubOneLaurentRemainder_le (N : ℕ) (v : ℝ) :
    |deriv (oneDivExpSubOneLaurentRemainder N) v| ≤
      (2 * (2 * N + 3 : ℕ) *
        ∑' m : ℕ, ((2 * Real.pi * (m + 1)) ^ (2 * N + 2))⁻¹) *
        |v| ^ (2 * N)

Uses 2 · Used by 1

Statement usesRemainder of the Laurent expansion of \(1/(e^v - 1)\)

Proof usesMittag-Leffler expansion of \(1/(e^u - 1)\)

Used byAsymptotic expansion of \(\sum 1/(n(n^x - 1))\) as \(x \to 0^+\)

TheoremGlobal remainder bound for the Laurent expansion of \(1/(e^v - 1)\)#✓fully proved

For every natural number \(N\) there is a constant \(C \ge 0\) such that for every real number \(v \neq 0\),

\[ \left| \frac{1}{e^v - 1} - \frac{1}{v} + \frac{1}{2} - \sum_{n=0}^{N-1} \frac{B_{2n+2}}{(2n+2)!} v^{2n+1} \right| \le C |v|^{2N+1}, \]

where \(B_k\) are the Bernoulli numbers.

theorem abs_one_div_exp_sub_one_sub_laurent_le (N : ℕ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ v : ℝ, v ≠ 0 →
      |1 / (Real.exp v - 1) - 1 / v + 1 / 2 -
          ∑ n ∈ Finset.range N,
            (bernoulli (2 * n + 2) : ℝ) / ((2 * n + 2).factorial : ℝ) *
              v ^ (2 * n + 1)| ≤
        C * |v| ^ (2 * N + 1)

Uses 1

Proof usesMittag-Leffler expansion of \(1/(e^u - 1)\)

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.