### Abstract

This entry builds upon the results about formal and analytic Dirichlet series to define the Hurwitz ζ function ζ(a,s) and, based on that, the Riemann ζ function ζ(s). This is done by first defining them for ℜ(z) > 1 and then successively extending the domain to the left using the Euler–MacLaurin formula.

Apart from the most basic facts such as analyticity, the following results are provided:

- the Stieltjes constants and the Laurent expansion of ζ(s) at s = 1
- the non-vanishing of ζ(s) for ℜ(z) ≥ 1
- the relationship between ζ(a,s) and Γ
- the special values at negative integers and positive even integers
- Hurwitz's formula and the reflection formula for ζ(s)
- the Hadjicostas–Chapman formula

The entry also contains Euler's analytic proof of the infinitude of primes, based on the fact that ζ(s) has a pole at s = 1.

### License

BSD License

### Topics

- Mathematics/Number theory
- Mathematics/Analysis

### Session Zeta_Function

- Zeta_Library
- Zeta_Function
- Zeta_Laurent_Expansion
- Hadjicostas_Chapman

### Depends on

- Bernoulli Numbers
- Dirichlet Series
- The Euler–MacLaurin Formula
- Evaluate Winding Numbers through Cauchy Indices

### Used by

- Kummer’s congruence
- Executable Randomized Algorithms
- Elementary Facts About the Distribution of Primes
- The Prime Number Theorem
- Dirichlet L-Functions and Dirichlet’s Theorem

## Cite

×

Zeta_Function-AFP

    @article{Zeta_Function-AFP,
      author  = {Manuel Eberl},
      title   = {The Hurwitz and Riemann ζ Functions},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/Zeta_Function.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 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 16, 2017 : Isabelle2017