Binet's formulas for the log-gamma function

Remarks

The integrand of the first formula is bounded near $t = 0$, since $\frac12 - \frac1t + \frac{1}{e^t - 1} = \frac{t}{12} + O(t^3)$. The first formula comes from integrating the integral representation of the digamma function. The second comes from the Abel–Plana summation formula, or from the first by a partial fraction expansion of $\frac{1}{e^t - 1}$. The function $\mu$ is called Binet's function; it is positive and decreasing on $(0, \infty)$ and tends to $0$ as $x \to \infty$. This limit is Stirling's formula for the gamma function on the real axis, and expanding $\frac12 - \frac1t + \frac{1}{e^t - 1}$ in powers of $t$ gives Stirling's series term by term. For example, the first term $\frac{t}{12}$ contributes $\int_0^\infty \frac{1}{12} e^{-zt}\,dt = \frac{1}{12z}$, the first correction in Stirling's series.

Going deeper

For a student

Binet's first formula is a Laplace transform, so Watson's lemma turns the Taylor series of its integrand directly into the asymptotic expansion of $\mu(z)$. The second formula is convenient for error bounds in the right half-plane, because the kernel $\frac{1}{e^{2\pi t} - 1}$ is explicit and positive. Both show that $\mu(x) \to 0$ monotonically, which gives sharp bounds such as $0 < \mu(x) < \frac{1}{12x}$ for $x > 0$.