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