7.9. The digamma function🔗

The original file defines the digamma function ad hoc, as the derivative of \log \circ \Gamma on the reals, and reproves the needed estimates. The real digamma function Real.digamma of Definition 3.1.4 now lives in the project's Mathlib-candidate library (CohnElkiesForMathlib.Analysis.SpecialFunctions.Gamma.Digamma), defined as the real part of Mathlib's Complex.digamma (as Real.Gamma is the real part of Complex.Gamma) and identified with the logarithmic derivative of Real.Gamma, together with its recurrence, the bounds \log(x-1) \le \psi(x) \le \log x, the harmonic representation \psi(m) = \lim_n(\log n - \sum_{k \le n}(m+k)^{-1}) and Gauss's integral representation (Lemma 3.1.7, listed as a TODO in Mathlib's digamma file). Mathlib (as of the pinned version) has Complex.digamma with its basic values and recurrence but no real digamma function and no series or asymptotic expansions.