0
$\begingroup$

For the purpose of formalisation in a theorem prover, I am looking for a simple definition of the analytic extension of the Hurwitz ζ function $\zeta(s,q)$ valid for all $s\in\mathbb{C}\setminus\{1\}$ and ideally a large set of value for $q$ (although $q \in (0;1]$ probably suffices).

There are two approaches that I am aware of:

  • Using a contour integral representation like in Tom Apostol's ‘Introduction to Analytic Number theory’
  • Using the convergent Newton sum representation given by Hasse in ‘Ein Summierungsverfahren für die Riemannsche ζ-Reihe’

Are there any other methods? Choosing the ‘right’ definition can make a huge difference in formal proofs, so: Which one is likely to be the ‘easiest’ or most elegant, or has the most rigorous and explicit proof?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

Summing by parts, using the binomial series and inverting the double sum works fine, obtaining

$$\zeta(s,a)-s \zeta(s,N) = \sum_{n=1}^{N-1} n ((n+a-1)^{-s}-(n+a)^{-s})\\+ \sum_{k=0}^\infty {-s \choose k+2} ((a-1)^{k+2} -a^{k+2}) \zeta(s+k+1,N)$$ Taking $a=1$ shows $(s-1)\zeta(s,N)$ is entire, from which you obtain that $\zeta(s,a)-s \zeta(s,N)$ and hence $(s-1)\zeta(s,a)$ is entire.

Improve this answer
$\endgroup$
4
  • $\begingroup$ Sorry, but could you please go into more detail here? I don't understand the steps here at all. $\endgroup$
    – Manuel Eberl
    Commented Jul 12, 2017 at 9:26
  • $\begingroup$ Is there perhaps some connection to the Euler–MacLaurin summation formula? $\endgroup$
    – Manuel Eberl
    Commented Jul 12, 2017 at 9:43
  • $\begingroup$ @ManuelEberl No. Use summation by parts and the binomial series to obtain $\displaystyle\zeta(s,a) = \sum_{n=0}^\infty (n+a)^{-s} = \sum_{n=0}^\infty (n+1) ((n+a)^{-s}-(n+a+1)^{-s})$ $\displaystyle =\sum_{n=1}^\infty n^{1-s} ((1+\frac{a-1}{n})^{-s}-(1+\frac{a}{n})^{-s})$ $ \displaystyle= \sum_{n=1}^\infty n^{1-s} \sum_{k=0}^\infty {-s \choose k} ((a-1)^k - a^k) n^{-k}$ then change the order of summation $\endgroup$
    – reuns
    Commented Jul 12, 2017 at 22:39
  • $\begingroup$ All right, thanks. I'll see what I can do with this. $\endgroup$
    – Manuel Eberl
    Commented Jul 13, 2017 at 23:21

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .