20 The Digamma Function
Earlier chapters (Thread HT, QG-Blackbody’s kinematic-block gap) recorded “Mathlib has no digamma/polygamma function” as a blocking gap, from a grep for the name digamma/polygamma in .lake/packages/mathlib/ (zero hits at pinned v4.19.0). That was the wrong question: Mathlib’s NumberTheory.Harmonic.GammaDeriv already computes deriv Real.Gamma in closed form at \(1\) and \(1/2\) (Bohr–Mollerup convexity; Legendre’s duplication formula) and at every positive integer. GppDigamma.digamma := deriv Gamma / Gamma makes the values below immediate corollaries.
\(\psi (1) = -\gamma \), the Euler–Mascheroni constant.
\(\psi (1/2) = -\gamma - 2\log 2\), via Legendre’s duplication formula (already differentiated in Mathlib).
\(\psi (n+1) = -\gamma + H_n\) (the \(n\)-th harmonic number), for every \(n\in \mathbb {N}\).
\(\psi (x+1) = \psi (x) + 1/x\), for \(x\) avoiding the poles of \(\Gamma \).
Honest boundary. This is the real-argument digamma function only. kinematic_block_v1.tex’s First Moment Theorem needs \(\mathrm{Re}\, \psi (1/2+i\lambda /2)\), the complex digamma along a vertical line — a further, separate extension, not attempted here. The Gauss integral representation of \(\psi \) at general real \(r\) (needed by Thread HT’s Archimedean Laplace transform) is likewise not yet established.