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?



Analytic extension of the Hurwitz ζ function
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.


