An attempt at formalizing facts on Euler products in Lean
Some results have by now made it into Mathlib.
Current projects:
- EulerProducts/Auxiliary.lean: auxiliary lemmas
- EulerProducts/Logarithm.lean: proves a logarithmic version of the Euler product formula for completely multiplicative arithmetic functions
- EulerProducts/LSeries.lean: convergence, derivatives, products of L-series
-
EulerProducts/PNT.lean: a reduction of the Prime Number Theorem
(in the version
$\psi(x) \sim x$ ) to a version of the Wiener-Ikehara Tauberian Theorem.