Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Perron's Formula

view this post on Zulip Email Gateway (Jun 26 2026 at 12:56):

From: Lawrence Paulson <lp15@cam.ac.uk>

I'm happy to announce yet another contribution from the ever prolific and entirely non-artificial Manuel.

Perron's Formula
Manuel Eberl

This entry provides a proof of Perron's Formula for a Dirichlet series.
The proofs mainly follow Tenenbaum's Introduction to Analytic and Probabilistic Number Theory and Titchmarsh's Theory of Functions.

The full abstract, including the mathematical formulas elided above, can be found in the entry itself:

https://isa-afp.org/entries/Perrons_Formula.html

Larry

Last updated: Jul 02 2026 at 07:34 UTC