Bernoulli polynomials, polylogarithms and Clausen functions

Bernoulli and Euler polynomials and their generating-function identities, Berndt's φ_r and power-difference series, Clausen functions, the inverse tangent integral and dilogarithm identities; results whose content is values of ζ, Dirichlet L or β functions belong to NumberTheory.

• Berndt's power-difference function φᵣ
• Clausen functions
• Dilogarithm identities
• Eulerian polynomials
• Inverting shift and difference operators

TheoremThe inverse tangent integral at \(\tan x\)#✓fully proved

Let \(x\) be a real number with \(|x| \le \pi/4\), and let \(P(x) = x \log|\tan x|\) for \(x \ne 0\) and \(P(0) = 0\). Then \(\cos x \ne 0\), the series \(T(x) = \sum_{k=0}^{\infty} (-1)^k \frac{\tan^{2k+1} x}{(2k+1)^2}\) (the inverse tangent integral of \(\tan x\)) and \(F(x) = \sum_{j=0}^{\infty} \frac{\sin((4j+2)x)}{(2j+1)^2}\) are both summable, and \(T(x) = P(x) + F(x)\).

theorem ramanujan_part1_ch9_entry17_sec (x : ℝ) (hx : |x| ≤ Real.pi / 4) :
    Real.cos x ≠ 0 ∧
      Summable (Entry32Lambertdivisor.chapter9Entry19TanTerm x) ∧
      Summable (Entry21Piseries2.chapter9Entry21SineTerm x) ∧
      (∑' k : ℕ, Entry32Lambertdivisor.chapter9Entry19TanTerm x k) =
        chapter9XLogAbsTan x +
          ∑' k : ℕ, Entry21Piseries2.chapter9Entry21SineTerm x k

Sources

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

Uses 2

Proof usesA series in even powers of \(\tan x\) with odd harmonic numbers · Ramanujan's sine series in odd powers of the tangent (Entry 32)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.