Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Concrete bounds for Chebyshev’...

Email Gateway (Sep 16 2024 at 15:44):

From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to announce yet another entry by the ever prolific Manuel Eberl. He derives explicit lower and upper bounds for Chebyshev's prime counting functions, using Stirling's formula as a starting point. Bertrand's postulate follows: for every x>1 the interval (x,2x) contains at least one prime.

https://www.isa-afp.org/entries/Chebyshev_Prime_Bounds.html

Larry Paulson

Last updated: Jan 04 2025 at 20:18 UTC