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.
20.1 The closing third of the First Moment Theorem
principal_series_blocks_v2.tex’s Theorem 6.1 (thm:moment) asserts
Its proof has three inputs. The results below are the third — the one that produces the \(1/8\) — and they are unconditional. Theorem 6.1 itself is not proved and is not stated in Lean.
\(e^{-t/2}/(1-e^{-t}) = 1/(2\sinh (t/2))\) for every \(t{\gt}0\).
\(\dfrac {1}{2\sinh 2u}\cdot \dfrac {1-\operatorname {sech}^2u}{4} = \dfrac {1}{16}\, \tanh u\, \operatorname {sech}^2u\) for every real \(u\). The paper performs this in one line as “the integrand collapses to \(\tanh u\operatorname {sech}^2u\)”; that line silently carries the substitution \(u=t/4\), and hence the constant \(1/16\) made explicit here.
\(\int _0^\infty \tanh u\, \operatorname {sech}^2u\, \dd u = 1/2\), by the fundamental theorem of calculus with antiderivative \(-1/(2\cosh ^2 u)\).
This is where Theorem 6.1’s \(1/8\) comes from.
Honest boundary. Two inputs remain, and neither is stated in Lean — not as an axiom, not as a sorry, not as a True-valued stub. First, the Fourier pair \(\frac{1}{2\pi }\int _{\mathbb {R}} P(\lambda )\cos (\lambda y)\dd \lambda = 1/(4\cosh ^2(y/2))\), used at \(y=0\) to give \(\frac{1}{2\pi }\int P=\frac14\) and at \(y=t/2\) to produce the integrand above; Mathlib has the Gaussian Fourier transform but nothing for \(\operatorname {sech}^2\). Second, Gauss’s integral representation \(\psi (s)=-\gamma +\int _0^\infty (e^{-t}-e^{-st})/(1-e^{-t})\dd t\), together with the complex digamma along \(\mathrm{Re}\, s=1/2\). The exchange of integration order between them is Tonelli on a positive integrand and is routine once both exist.