ArithmeticFunction.LSeries_powR_eq

@[blueprint  "LSeries_powR_eq"  (title := "LSeries powR eq")  (statement := /-- $L(\text{pow}^R(\nu), s) = \zeta(s - \nu)$ for $\Re(s - \nu) > 1$.  \begin{verbatim}  This is IK (1.27).  \end{verbatim}  -/)  (proof := /--  The function $\text{pow}^R(\nu)$ is defined as $n \mapsto n^\nu$ for $n \neq 0$ and $0$ for $n = 0$. The L-series of $\text{pow}^R(\nu)$ at $s$ is given by the sum $\sum_{n=1}^{\infty} n^{\nu - s}$. This series converges to the Riemann zeta function $\zeta(s - \nu)$ for $\Re(s - \nu) > 1$, since the zeta function is defined as $\zeta(s) = \sum_{n=1}^{\infty} n^{-s}$ for $\Re(s) > 1$. Therefore, we have $L(\text{pow}^R(\nu), s) = \zeta(s - \nu)$ under the condition that $\Re(s - \nu) > 1$.  -/)]lemma LSeries_powR_eq (ν : ℂ) {s : ℂ} (hs : 1 < (s - ν).re) :    LSeries (powR ν) s = riemannZeta (s - ν) := by  convert ( LSeries_congr _ _ ) using 1;  · rw [ zeta_eq_tsum_one_div_nat_cpow hs ];    · refine tsum_congr fun n => ?_;      by_cases hn : n = 0      · simp only [LSeries.term, hn, one_div, CharP.cast_eq_zero, ↓reduceIte, inv_eq_zero, Complex.cpow_eq_zero_iff,          ne_eq, true_and]        exact sub_ne_zero_of_ne (by rintro rfl; norm_num at hs)      · simp only [one_div];        rw [← Complex.cpow_neg, neg_sub, Complex.cpow_sub];        · exact Eq.symm (LSeries.term_of_ne_zero hn (fun n ↦ ↑n ^ ν) s)        · exact cast_ne_zero.mpr hn  · unfold ArithmeticFunction.powR; aesop;