ArithmeticFunction.LSeries_sigma_eq_riemannZeta_mul

@[blueprint  "LSeries_sigma_eq_riemannZeta_mul"  (title := "LSeries sigma eq riemannZeta mul")  (statement := /-- $\zeta(s)\zeta(s - \nu) = \sum_{n=1}^{\infty} \sigma_\nu(n) n^{-s}$ for $\Re(s) > 1$ and $\Re(s - \nu) > 1$. -/)  (proof := /--  The divisor power sum function $\sigma_\nu$ is the Dirichlet convolution of the constant function $1$ (i.e., $\zeta$) and the power function $n \mapsto n^\nu$. The L-series of a Dirichlet convolution is the product of the L-series of the individual functions. Since $L(1, s) = \zeta(s)$ and $L(n \mapsto n^\nu, s) = \zeta(s - \nu)$, we have $L(\sigma_\nu, s) = \zeta(s) \cdot \zeta(s - \nu)$ for $\Re(s) > 1$ and $\Re(s - \nu) > 1$.  -/)]theorem LSeries_sigma_eq_riemannZeta_mul (ν : ℂ) {s : ℂ} (hs : 1 < s.re) (hsν : 1 < (s - ν).re) :    LSeries (↗(σᴿ ν)) s = riemannZeta s * riemannZeta (s - ν) := by  rw [← ArithmeticFunction.LSeries_zeta_eq_riemannZeta hs, ← LSeries_powR_eq ν hsν, sigmaR_eq_zeta_mul_powR];  apply ArithmeticFunction.LSeries_mul  · apply (ArithmeticFunction.abscissaOfAbsConv_zeta.trans_lt _)    exact_mod_cast hs  · apply lt_of_le_of_lt (abscissa_powR_le ν)    rw[Complex.sub_re] at hsν    exact_mod_cast (by linarith)