How to show tetration integral converges

Question

I was wondering if others could review my proof the following integral converges and tell me if it's ok? W is the Lambert-W function.

$$-\int_0^{1}\frac{\text{W}[-\log(\sin(z))]}{\log[\sin(z)]}dz$$

A plot of the function from $(0,\pi)$ is shown below.

Proof:

Near zero, $\sin(z)\sim z$ so we can consider $$\int_0^{1}\frac{\text{W}[-\log(z)]}{\log[z]}dz$$ It suffices then to show $$\lim_{z\to 0^+} \frac{\text{W}(-log(z))}{log(z)}=0 $$ Since we have the indeterminant form $\frac{\infty}{\infty}$, applying L'Hopital's rule: $$ \frac{\frac{d}{dz}\text{W}(-log(z))}{\frac{d}{dz}\log(z)}=\frac{\text{W}(-\log(z))}{\log(z)(1+\text{W}(-\log(z))} $$ and this is where my logic is a bit unorthodox: We still have the indeterminant form $\frac{\infty}{\infty}$ however, the denominator approaches $\infty+\infty$ so the expression becomes much smaller than $1/z$ so that I may conclude the limit is zero.

Is this rigorous enough or is there a more appropriate way to prove the limit is zero?

Answer 1

I don't really see how you conclude the limit is zero from where you left off. There appears to be a lot of handwaving involved. Alternatively, multiply the integrand by $-1$. One can then see the integrand is then the inverse of $y=\arcsin(x^{1/x})$. Letting $y\to0^+$, one can see that $x^{1/x}=\exp(\ln(x)/x)\to0$, so that $\ln(x)/x\to-\infty$, which clearly happens as $x\to0^+$. So the limit exists and is zero.

Answer 2

Let me go over Beautiful Art's way above to make sure I understand:

We need to prove:

$$ -\int_0^1\frac{\text{W}(-\log(\sin(x)))}{\log(\sin(x))}dx $$ converges. But there is no need to do so directly if we can show the integrand approaches a limit as x goes to zero as the integrand is well-defined otherwise. Letting $$ y=-\frac{\text{W}(-\log(\sin(x)))}{\log(\sin(x))} $$ then, surprisingly, $x=\displaystyle\arcsin((1/y)^{-1/y})=\arcsin(y^{1/y})$ so we have $$\displaystyle x=\arcsin(y^{1/y})$$ and we wish to know what $y$ is as x goes to zero or equivalently: $$ \lim_{x\to 0^+}\left(x=\arcsin(y^{1/y})\right) $$ Clearly when $x\to 0$ we must have the argument of $\arcsin$ go to zero as well or $e^{\frac{1}{y}\log(y)}$ must go to zero. But the exponential goes to zero when $\frac{1}{y}\log(y)\to -\infty$ and this happens when $y\to 0$.

So we have shown that when $y\to 0$, we have $x\to 0$ and conversely:

$$ \lim_{x\to 0^+} -\frac{\text{W}(-\log(\sin(x)))}{\log(\sin(x))}=0 $$

and this shows the integral is bounded so that the integral converges.