|
Dirichlet
L-Functions
and
Dirichlet's
Theorem
Title: |
Dirichlet L-Functions and Dirichlet's Theorem |
Author:
|
Manuel Eberl
|
Submission date: |
2017-12-21 |
Abstract: |
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). |
BibTeX: |
@article{Dirichlet_L-AFP,
author = {Manuel Eberl},
title = {Dirichlet L-Functions and Dirichlet's Theorem},
journal = {Archive of Formal Proofs},
month = dec,
year = 2017,
note = {\url{http://isa-afp.org/entries/Dirichlet_L.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Bertrands_Postulate, Dirichlet_Series, Landau_Symbols, Zeta_Function |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|