Dirichlet Series

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.