An attempt at formalizing facts on Euler products and L-series more generally in Lean
Most of the results developed here have by now made it into Mathlib, most notably a proof of Drichlet's Theorem on Primes in Residue Classes.
What is currently left in this repository are some bits and pieces that were not needed for the big result, but may still be useful.
Contents:
- EulerProducts/Auxiliary.lean: auxiliary lemmas
- EulerProducts/EulerProduct.lean: Euler products formulas for L-series of weakly or completely multiplicative sequences
- EulerProducts/DirichletLSeries.lean: results on L-series of Dirichlet characters and specific arithmetic functions (like the Möbius and von Mangoldt functions)
- EulerProducts/PNT.lean: a reduction of an asymptotic version of Dirichlet's Theorem to a version of the Wiener-Ikehara Tauberian Theorem. Note that the Wiener-Ikehara Theorem is proved in PNT+.