
Dirichlet
Series
Title: 
Dirichlet Series 
Author:

Manuel Eberl

Submission date: 
20171012 
Abstract: 
This entry is a formalisation of much of Chapters 2, 3, and 11 of
Apostol's “Introduction to Analytic Number
Theory”. This includes:  Definitions and
basic properties for several numbertheoretic functions (Euler's
φ, Möbius μ, Liouville's λ,
the divisor function σ, von Mangoldt's
Λ)
 Executable code for most of these
functions, the most efficient implementations using the factoring
algorithm by Thiemann et al.
 Dirichlet products and formal Dirichlet series
 Analytic results connecting convergent formal Dirichlet
series to complex functions
 Euler product
expansions
 Asymptotic estimates of
numbertheoretic functions including the density of squarefree
integers and the average number of divisors of a natural
number
These results are useful as a basis for
developing more numbertheoretic results, such as the Prime Number
Theorem. 
BibTeX: 
@article{Dirichlet_SeriesAFP,
author = {Manuel Eberl},
title = {Dirichlet Series},
journal = {Archive of Formal Proofs},
month = oct,
year = 2017,
note = {\url{http://isaafp.org/entries/Dirichlet_Series.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
Euler_MacLaurin, Landau_Symbols, Polynomial_Factorization 
Used by: 
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.

