<s>[INST] $\int_0^{\frac{\pi}{2}}x\cot(x)dx$ and $ \lim_{m \rightarrow \infty}\log\left( e^{2m}\left(\frac{(2m-1)!!}{(2m+1)^m}\right)^2\right)$. I'm trying to evaluate the integral, but in doing so have stumbled upon the limit, which I don't know whether it exists, and if so how to resolve it (and whether I've derived the relationship between the integral and limit correctly  [see below]). 
Derivation: First, use the cotangent formula: $$\cot(x)=\sum_{-\infty\le n\le\infty}\frac{1}{x+\pi n},$$
and apply it to the integral:
$$\int_0^{\frac{\pi}{2}}x\cot(x)dx=\sum_{-\infty\le n\le\infty}\int_0^{\frac{\pi}{2}}\frac{x}{x+\pi n}dx$$
$$=\sum_{-\infty\le n\le\infty}\int_{n \pi}^{\pi \left(n+\frac{1}{2}\right)}\frac{u- \pi n}{u}du$$
$$=\sum_{-\infty\le n\le\infty}[u-\pi n \log(u)]_{n \pi}^{\pi \left(n+\frac{1} {2}\right)},$$
and rearranging,
$$=\sum_{-\infty\le n\le\infty}\frac{\pi}{2}-\pi n \log\left(\frac{2n+1}{2n}\right)$$
$$=\frac{\pi}{2}\sum_{-\infty\le n\le\infty}  \log\left( e\left(\frac{2n}{2n+1}\right)^{2n}\right)$$
$$=\frac{\pi}{2}  \log\left( \prod_{-\infty\le n\le\infty} e\left(\frac{2n}{2n+1}\right)^{2n}\right).$$
Note that $$\prod_{-\infty\le n\le\infty} \left(\frac{2n}{2n+1}\right)^{2n}=  \prod_{1\le n\le\infty} \left(\frac{2n}{2n+1}\right)^{2n}\left(\frac{-2n}{-2n+1}\right)^{-2n} $$
$$=  \prod_{1\le n\le\infty} \left(\frac{2n-1}{2n+1}\right)^{2n} $$
$$=\left(\frac{1^1}{3^1}\cdot\frac{3^2}{5^2}\cdot\frac{5^3}{7^3}\cdots\right)^2=\lim_{m \rightarrow \infty}\left(\frac{(2m-1)!!}{(2m+1)^m}\right)^2.$$
Thus the original integral is equal to
$$\frac{\pi}{2}  \lim_{m \rightarrow \infty}\log\left( e^{2m+1}\left(\frac{(2m-1)!!}{(2m+1)^m}\right)^2\right).$$
 [/INST] IMHO, it will be simpler if one integrate the integral by parts. Using answers from the question Evaluate: $\int_0^{\pi} \ln \left( \sin \theta \right) d\theta$, we have
$$\int_0^{\frac{\pi}{2}} x \cot x dx = \int_0^{\frac{\pi}{2}} x (\log \sin x)' dx
= \Big[x \log \sin x\Big]_0^{\frac{\pi}{2}} - \int_0^{\frac{\pi}{2}} \log\sin x dx\\
= - \int_0^{\frac{\pi}{2}} \log\sin x dx
= \frac{\pi}{2}\log 2$$
</s>