2.3. The Riemann zeta function via the Mellin transform
The Riemann zeta function is the central player of these notes, so we recall how its special values are computed. The tool is a general analytic-continuation result for the Mellin transform.
- No associated Lean code or declarations.
Let f:\R_{\geq 0}\to\R be a rapidly decreasing \cC^{\infty}-function (so f
and all its derivatives decay exponentially at \infty), and let
\Gamma(s)=\int_0^\infty e^{-t}t^{s-1}\,dt be the Gamma function. The Mellin
transform of f is
L(f,s) := \frac{1}{\Gamma(s)}\int_0^\infty f(t)\,t^{s-1}\,dt,\qquad s\in\C.
It converges to a holomorphic function for \mathrm{Re}(s)>0, admits an analytic
continuation to all of \C, and satisfies, for every n\geq 0,
L(f,-n) = (-1)^n f^{(n)}(0).
The key step is the recursion
L(f,s) = -L(f',s+1),\qquad \mathrm{Re}(s)>1,
obtained by integration by parts. Taking u=f(t) and dv=t^{s-1}\,dt, so
v=t^s/s, gives
\int_0^\infty f(t)t^{s-1}\,dt = \big[f(t)t^s/s\big]_0^\infty -
\tfrac1s\int_0^\infty f'(t)\,t^s\,dt. The boundary terms vanish: at \infty by
the rapid decay of f, at 0 because \mathrm{Re}(s)>1. Dividing by
\Gamma(s) and using the functional equation \Gamma(s+1)=s\,\Gamma(s) turns the
remaining integral into -\Gamma(s+1)^{-1}\int_0^\infty f'(t)t^{(s+1)-1}\,dt =
-L(f',s+1), which is the displayed recursion. Since f' is again rapidly
decreasing, the right-hand side is holomorphic on \mathrm{Re}(s)>-1, so the
recursion provides the analytic continuation of L(f,s) one strip to the left;
iterating with f',f'',\dots continues it to all of \C. Applying the recursion
n+1 times gives L(f,-n)=(-1)^{n+1}L(f^{(n+1)},1), and since
L(g,1)=\Gamma(1)^{-1}\int_0^\infty g(t)\,dt=\int_0^\infty g(t)\,dt, the
fundamental theorem of calculus yields
L(f,-n)=(-1)^{n+1}\int_0^\infty f^{(n+1)}(t)\,dt=(-1)^{n+1}\big[-f^{(n)}(0)\big]
=(-1)^n f^{(n)}(0), using once more that f^{(n)} vanishes at \infty.
To recover \zeta we apply this to the generating function of the Bernoulli
numbers,
f(t) = \frac{t}{e^t-1} = \sum_{n\geq 0}B_n\frac{t^n}{n!}.
The Bernoulli numbers B_n are rational, with B_0=1, B_1=-\tfrac12,
B_2=\tfrac16, B_3=0, B_4=-\tfrac1{30},\dots, and B_k=0 for odd k\geq 3.
The function f(t)=t/(e^t-1) and all of its derivatives decay exponentially as
t\to\infty.
For t>0 expand as a geometric series
f(t)=t(e^{-t}+e^{-2t}+e^{-3t}+\cdots)=:tF(t). Differentiating f=tF
repeatedly via the Leibniz rule gives f^{(n)}(t)=nF^{(n-1)}(t)+tF^{(n)}(t). Each
F^{(m)}(t)=(-1)^m(e^{-t}+2^m e^{-2t}+3^m e^{-3t}+\cdots) is, term by term,
exponentially small, dominated by its leading term (-1)^m e^{-t}. Hence
f^{(n)}(t)\sim(-1)^n t e^{-t} as t\to\infty, which decays exponentially.
For f(t)=t/(e^t-1) as above, (s-1)\zeta(s) = L(f,s-1). This rests on
Definition 2.1.1 and Theorem 2.3.1.
Substituting t\mapsto nt in the integral defining \Gamma(s) gives
n^{-s}=\Gamma(s)^{-1}\int_0^\infty e^{-nt}t^{s-1}\,dt. Summing over n\geq 1
for \mathrm{Re}(s) large and exchanging sum and integral,
\zeta(s) = \frac{1}{\Gamma(s)}\sum_{n\geq 1}\int_0^\infty e^{-nt}t^{s-1}\,dt
= \frac{1}{\Gamma(s)}\int_0^\infty\Big(\sum_{n\geq 1}e^{-nt}\Big)\,t\cdot t^{s-2}\,dt.
The geometric series gives \sum_{n\geq 1}e^{-nt}=1/(e^t-1), so the integrand is
\big(t/(e^t-1)\big)t^{s-2}=f(t)t^{(s-1)-1}. Comparing with the definition of the
Mellin transform at the argument s-1 (whose \Gamma-normalisation is
\Gamma(s-1)=\Gamma(s)/(s-1)) yields \zeta(s)=L(f,s-1)/(s-1), i.e.
(s-1)\zeta(s)=L(f,s-1).
-
riemannZeta_neg_nat_eq_bernoulli'[complete]
For every n\geq 0,
\zeta(-n) = -\frac{B_{n+1}}{n+1}.
In particular \zeta(-n)\in\Q, and \zeta(-n)=0 when n\geq 2 is even. This
rests on Lemma 2.3.3, Theorem 2.3.1 and
Lemma 2.3.2. (At n=0 the formula implicitly uses the
convention B_1=+\tfrac12; mathlib's riemannZeta_neg_nat_eq_bernoulli' states
exactly this, via the Bernoulli numbers B'_j with B'_1=+\tfrac12.)
Lean code for Corollary2.3.4●1 theorem
Associated Lean declarations
-
riemannZeta_neg_nat_eq_bernoulli'[complete]
-
riemannZeta_neg_nat_eq_bernoulli'[complete]
-
theoremdefined in Mathlib/NumberTheory/LSeries/HurwitzZetaValues.leancomplete
theorem riemannZeta_neg_nat_eq_bernoulli' (k : ℕ) : riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
theorem riemannZeta_neg_nat_eq_bernoulli' (k : ℕ) : riemannZeta (-↑k) = -↑(bernoulli' (k + 1)) / (↑k + 1)
Value of Riemann zeta at `-ℕ` in terms of `bernoulli'`.
By Lemma 2.3.2, f is admissible in
Theorem 2.3.1, so L(f,-m)=(-1)^m f^{(m)}(0). The Taylor
expansion f(t)=\sum_{j\geq 0}B_j t^j/j! gives f^{(m)}(0)=B_m, hence
L(f,-m)=(-1)^m B_m. Now evaluate the identity (s-1)\zeta(s)=L(f,s-1) from
Lemma 2.3.3 at s=-n: the left-hand side is
(-n-1)\zeta(-n), and the right-hand side is L(f,-n-1)=(-1)^{n+1}B_{n+1}.
Therefore \zeta(-n)=(-1)^{n+1}B_{n+1}/(-n-1)=-B_{n+1}/(n+1). Since the B_j
are rational, so is \zeta(-n); and as B_{n+1}=0 for n+1\geq 3 odd, i.e.
for n\geq 2 even, the value vanishes there.