Abstract

This entry derives explicit lower and upper bounds for Chebyshev’s prime counting functions psi and theta. The proofs work by careful estimation of psi(x) with Stirling’s formula as a starting point, to prove the bound for all sufficiently large x, followed by brute-force approximation for the remaining values of x.

An easy corollary of this is Bertrand’s postulate, i.e. the fact that for any x > 1 the interval (x, 2x) contains at least one prime (a fact that has already been shown in the AFP using weaker bounds for psi and theta).

BibTeX

@article{Chebyshev_Prime_Bounds-AFP,
  author  = {Manuel Eberl},
  title   = {Concrete bounds for {C}hebyshev’s prime counting functions},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/Chebyshev_Prime_Bounds.html},
             Formal proof development},
  ISSN    = {2150-914x},
}