### 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.

### License

BSD License

### Topics

- Mathematics/Number theory

### Session Dirichlet_Series

- Dirichlet_Misc
- Multiplicative_Function
- Dirichlet_Product
- Dirichlet_Series
- Moebius_Mu
- More_Totient
- Liouville_Lambda
- Divisor_Count
- Arithmetic_Summatory
- Partial_Summation
- Euler_Products
- Dirichlet_Series_Analysis
- Arithmetic_Summatory_Asymptotics
- Dirichlet_Efficient_Code

### Depends on

- The Euler–MacLaurin Formula
- Landau Symbols
- Polynomial Factorization

### Used by

- Lambert Series
- Finite Fields
- Gauss Sums and the Pólya–Vinogradov Inequality
- Dirichlet L-Functions and Dirichlet’s Theorem
- The Hurwitz and Riemann ζ Functions

### Auto-related entries

- Three Squares Theorem
- Prime Number Theorem with Remainder Term
- Positional Notation for Natural Numbers in an Arbitrary Base
- Digit Expansions
- Elementary Facts About the Distribution of Primes

## Cite

×

Dirichlet_Series-AFP

    @article{Dirichlet_Series-AFP,
      author  = {Manuel Eberl},
      title   = {Dirichlet Series},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Dirichlet_Series.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 16, 2017 : Isabelle2017