Dirichlet Series

Title:	Dirichlet Series
Author:	Manuel Eberl
Submission date:	2017-10-12
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 number-theoretic 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 number-theoretic 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 number-theoretic results, such as the Prime Number Theorem.
BibTeX:	@article{Dirichlet_Series-AFP, author = {Manuel Eberl}, title = {Dirichlet Series}, journal = {Archive of Formal Proofs}, month = oct, year = 2017, note = {\url{http://isa-afp.org/entries/Dirichlet_Series.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Euler_MacLaurin, Landau_Symbols, Polynomial_Factorization
Used by:	Dirichlet_L, Gauss_Sums, 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.