Dirichlet L-Functions and Dirichlet's Theorem


Title: Dirichlet L-Functions and Dirichlet's Theorem
Author: Manuel Eberl
Submission date: 2017-12-21

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 ph (mod n).

  author  = {Manuel Eberl},
  title   = {Dirichlet L-Functions and Dirichlet's Theorem},
  journal = {Archive of Formal Proofs},
  month   = dec,
  year    = 2017,
  note    = {\url{https://isa-afp.org/entries/Dirichlet_L.html},
            Formal proof development},
  ISSN    = {2150-914x},
License: BSD License
Depends on: Bertrands_Postulate, Dirichlet_Series, Finitely_Generated_Abelian_Groups, Landau_Symbols, Zeta_Function
Used by: Gauss_Sums