Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] [ExternalEmail] AFP 2018


view this post on Zulip 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: Mar 28 2024 at 20:16 UTC