
Dirichlet
LFunctions
and
Dirichlet's
Theorem
Title: 
Dirichlet LFunctions and Dirichlet's Theorem 
Author:

Manuel Eberl

Submission date: 
20171221 
Abstract: 
This article provides a formalisation of Dirichlet characters
and Dirichlet Lfunctions including proofs of
their basic properties – most notably their analyticity,
their areas of convergence, and their nonvanishing for ℜ(s)
≥ 1. All of this is built in a very highlevel style using
Dirichlet series. The proof of the nonvanishing 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). 
BibTeX: 
@article{Dirichlet_LAFP,
author = {Manuel Eberl},
title = {Dirichlet LFunctions and Dirichlet's Theorem},
journal = {Archive of Formal Proofs},
month = dec,
year = 2017,
note = {\url{http://isaafp.org/entries/Dirichlet_L.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Bertrands_Postulate, Dirichlet_Series, Landau_Symbols, Zeta_Function 
Used by: 
Gauss_Sums 
