Email Gateway (Aug 22 2022 at 18:00): Email Gateway (Aug 22 2022 at 18:00):From: Gerwin.Klein@data61.csiro.au
It looks like I forgot this one in the list of development entries:
Dirichlet L-Functions and Dirichlet's Theorem
by Manuel Eberl
https://www.isa-afp.org/entries/Dirichlet_L.html
This article provides a formalisation of Dirichlet characters and Dirichlet L-functions including proofs of their basic properties – most notably their analyticity, their areas of convergence, and their non-vanishing for ℜ(s) ≥ 1. All of this is built in a very high-level style using Dirichlet series. The proof of the non-vanishing follows a very short and elegant proof by Newman, which we attempt to reproduce faithfully in a similar level of abstraction in Isabelle.
This also leads to a relatively short proof of Dirichlet’s Theorem, which states that, if h and n are coprime, there are infinitely many primes p with p ≡ h (mod n).
Apologies to Manuel!
Gerwin
Last updated: Nov 21 2024 at 12:39 UTC