This article provides a short proof of the Prime Number
Theorem in several equivalent forms, most notably
π(*x*) ~ *x*/ln
*x* where π(*x*) is the
number of primes no larger than *x*. It also
defines other basic number-theoretic functions related to primes like
Chebyshev's functions ϑ and ψ and the
“*n*-th prime number” function
p_{n}. We also show various
bounds and relationship between these functions are shown. Lastly, we
derive Mertens' First and Second Theorem, i. e.
∑_{p≤x}
ln *p*/*p* = ln
*x* + *O*(1) and
∑_{p≤x}
1/*p* = ln ln *x* + M +
*O*(1/ln *x*). We also give
explicit bounds for the remainder terms. The proof
of the Prime Number Theorem builds on a library of Dirichlet series
and analytic combinatorics. We essentially follow the presentation by
Newman. The core part of the proof is a Tauberian theorem for
Dirichlet series, which is proven using complex analysis and then used
to strengthen Mertens' First Theorem to
∑_{p≤x}
ln *p*/*p* = ln
*x* + c + *o*(1).
A variant of this proof has been formalised before by
Harrison in HOL Light, and formalisations of Selberg's elementary
proof exist both by Avigad *et al.* in Isabelle and
by Carneiro in Metamath. The advantage of the analytic proof is that,
while it requires more powerful mathematical tools, it is considerably
shorter and clearer. This article attempts to provide a short and
clear formalisation of all components of that proof using the full
range of mathematical machinery available in Isabelle, staying as
close as possible to Newman's simple paper proof. |