### Abstract

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).

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Prime_Distribution_Elementary

- Prime_Distribution_Elementary_Library
- More_Dirichlet_Misc
- Primes_Omega
- Primorial
- Lcm_Nat_Upto
- Shapiro_Tauberian
- Partial_Zeta_Bounds
- Moebius_Mu_Sum
- Elementary_Prime_Bounds
- Summatory_Divisor_Sigma_Bounds
- Selberg_Asymptotic_Formula
- PNT_Consequences

### Depends on

- The Prime Number Theorem
- The Hurwitz and Riemann ζ Functions

### Used by

- Irrationality Criteria for Series by Erdős and Straus
- The Irrationality of ζ(3)
- Selected Problems from the International Mathematical Olympiad 2019

### Auto-related entries

- Prime Number Theorem with Remainder Term
- Gauss Sums and the Pólya–Vinogradov Inequality
- Dirichlet Series

## Cite

×

Prime_Distribution_Elementary-AFP

    @article{Prime_Distribution_Elementary-AFP,
      author  = {Manuel Eberl},
      title   = {Elementary Facts About the Distribution of Primes},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Prime_Distribution_Elementary.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Feb 22, 2019 : Isabelle2018