EulerProducts
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.
Apart from the uniqueness result for L-series, 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/LSeriesUnique.lean: a converging L-series determines its coefficients
- 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+.