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.
  author  = {Manuel Eberl},
  title   = {Dirichlet Series},
  journal = {Archive of Formal Proofs},
  month   = oct,
  year    = 2017,
  note    = {\url{https://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