An attempt at formalizing facts on Euler products and L-series more generally in Lean
Some results have by now made it into Mathlib.
Current projects:
- 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 the Prime Number Theorem (in the version
$\psi(x) \sim x$ ) to a version of the Wiener-Ikehara Tauberian Theorem. This also contains a proof of the non-vanishing of Dirichlet L-functions of nontrivial characters along the lineRe s = 1. This is material that was created in the framework of the DirichletNonvanishing project. The non-vanishing is then used to give a proof (the reduction) of Dirichlet's Theorem (to the Wiener-Ikehara Theorem), in a PNT-like version.