Elementary Facts About the Distribution of Primes


Title: Elementary Facts About the Distribution of Primes
Author: Manuel Eberl
Submission date: 2019-02-21

This entry is a formalisation of Chapter 4 (and parts of Chapter 3) of Apostol's Introduction to Analytic Number Theory. The main topics that are addressed are properties of the distribution of prime numbers that can be shown in an elementary way (i. e. without the Prime Number Theorem), the various equivalent forms of the PNT (which imply each other in elementary ways), and consequences that follow from the PNT in elementary ways. The latter include, most notably, asymptotic bounds for the number of distinct prime factors of n, the divisor function d(n), Euler's totient function φ(n), and lcm(1,…,n).

  author  = {Manuel Eberl},
  title   = {Elementary Facts About the Distribution of Primes},
  journal = {Archive of Formal Proofs},
  month   = feb,
  year    = 2019,
  note    = {\url{https://isa-afp.org/entries/Prime_Distribution_Elementary.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Prime_Number_Theorem, Zeta_Function
Used by: IMO2019, Irrational_Series_Erdos_Straus, Zeta_3_Irrational