Email Gateway (Aug 22 2022 at 18:33): Email Gateway (Aug 22 2022 at 18:33):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
there are new results in the AFP about prime counting.
The Prime Number Theorem
by Manuel Eberl and Lawrence C. Paulson
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 pn. 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.
For more details, have a look at:
https://www.isa-afp.org/entries/Prime_Number_Theorem.html
Many thanks to Manual and Larry,
René
Last updated: Nov 21 2024 at 12:39 UTC