Spence function

[Albert Chan]

From [VA] SRC #010 - Pi Day 2022 Special

(03-17-2022 02:54 PM)Albert Chan Wrote:  \(\displaystyle \ln(\pi) = \int_0^{1/2} \left(
\frac{1}{y} + \frac{\pi (2y-1)}{\tan(\pi y)}
\right) dy\)

Wolfram Alpha proved this, with closed-form anti-derivative !

Only the midde term is troublesome. Lets get integral without middle term.

∫(1/y - pi/tan(pi*y) dy) = ln(y) - ln(sin(pi*y)) + C1 = -ln(sinc(pi*y)) + C2
∫(1/y - pi/tan(pi*y), y=0..1/2) = preval(-ln(sinc(pi*y)), 0, 1/2, y) = ln(pi) - ln(2)

For middle term integral, let x = pi*y, dx = pi dy

∫(2*pi*y / tan(pi*y), y=0..1/2) = 2/pi * ∫(x/tan(x), x=0 .. pi/2)

This reduced the proof to ∫(x/tan(x), x=0 .. pi/2) = pi/2*ln(2) ≈ 1.0888

∫(x/tan(x) dx) = ∫(x*i/tanh(x*i) dx) = ∫(z/tanh(z) dz) / i, where z=x*i

f = z/tanh(z) = z * cosh(z)/sinh(z) = z * (1+u)/(1-u), where u = e^(-2z)

To get (1-u) denominator, lets try ln(1-u)'

ln(1-u)' = 1/(1-u) * (1-u)' = 2u/(1-u)
(z*ln(1-u))' = ln(1-u) + z * ((1+u)-(1-u)) / (1-u) = ln(1-u) + f - z

Li2(u)' = -ln(1-u)/u * u' = 2*ln(1-u)

f = (z*ln(1-u))' + z - Li2(u)'/2
F = z*ln(1-u) + z^2/2 - Li2(u)/2       // = ∫(z/tanh(z) dz)

F(pi/2*i) = i*(pi/2*ln(2)) + (pi/2*i)^2/2 - Li2(-1)/2       // Li2(-1) = -pi^2/12
             = i*(pi/2*ln(2)) - pi^2/8 + pi^2/24

F(0*i) = limit(z*ln(1-exp(-2z)), z=0) + 0 - Li2(1)/2       // Li2(1) = ζ(2) = pi^2/6
         = 0 - pi^2/12

∫(x/tan(x), x=0..pi/2) = (F(pi/2*i) - F(0*i)) / i = pi/2*ln(2)       QED

---

It would be nice if F(0) = 0, avoiding calculation of limits.

For z = 0*i to pi/2*i, we have log(e^(2z)) = 2z. Let U = e^(2z):

f = z*(1+u)/(1-u) = -z*(1+U)/(1-U)

Li2(1-U)'
= -ln(1-(1-U)) / (1-U) * (1-U)'
= ln(U) / (1-U) * (2U)
= ln(U) / (1-U) * ((1+U) - (1-U))
= 2z*(1+U)/(1-U) - 2z         // NOTE: -pi/2 < im(z) ≤ pi/2
= -2f - 2z

f = -z - Li2(1-U)'/2
F = -z^2/2 - Li2(1-U)/2       // = ∫(t/tanh(t), t = 0 .. z), -pi/2 < im(z) ≤ pi/2

F(pi/2*i) = -(pi/2*i)^2/2 - Li2(2)/2       // Li2(2) = pi^2/4 - i*(pi*ln(2))

∫(x/tan(x), x=0..pi/2) = F(pi/2*i)/i = pi/2*ln(2)       QED