Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Prime number theorem with classical remainder ...

Email Gateway (Feb 16 2023 at 15:14):

From: Meow Mew <mmew78272@gmail.com>
Does Isabelle have a formalization of the prime number theorem with
O(exp(-c * sqrt(ln n))) remainder item? I am working towards it. The only
result I found in the AFP entry has the form \psi x ~ x and doesn't have a
remainder item estimation. The version that I will formalize will use
Perron's formula and non-zero region of the zeta function, instead of the
Newman-Ingham "Tauberian" method.

Email Gateway (Feb 16 2023 at 15:36):

From: Manuel Eberl <manuel@pruvisto.org>
No, we don't have this, but it would of course be lovely to have it. It's been on my long-time "nice to have but no concrete plans to do it" list.

Seeing as I did the formalisation of the zeta function and the PNT that we do have, I'd be happy to help if you need anything.

I would also be interested in learning what context you are doing this work in (i.e. do you need this result for something or what brought this to your attention?)

Cheers,

Manuel

Last updated: Apr 24 2024 at 16:18 UTC