Dirichlet Series (Q7361731)

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.