ArithmeticFunction.LSeries_d_summable

@[blueprint  "LSeries_d_summable"  (title := "LSeries d summable")  (statement := /-- The L-series for $d_k$ is summable for $\Re(s) > 1$. -/)  (proof := /--  Since $d_k$ is defined as the $k$-fold Dirichlet convolution of $\zeta$, and we know that the L-series of $\zeta$ converges for $\Re(s) > 1$, it follows that the L-series of $d_k$ also converges for $\Re(s) > 1$. This is because the convolution of functions with convergent L-series will also have a convergent L-series in the same region. Therefore, we can conclude that $L(d_k, s)$ is summable for $\Re(s) > 1$.  -/)]theorem LSeries_d_summable (k : ℕ) {s : ℂ} (hs : 1 < s.re) :      LSeriesSummable (↗(d k : ArithmeticFunction ℂ)) s := by  induction k with  | zero =>    simp only [d_zero, natCoe_one, one_eq_delta]    exact (hasSum_single 1 fun n hn => by simp [LSeries.term_delta, hn]).summable  | succ k ih =>    rw [(LSeriesSummable_congr s (fun {n} _ => show (d (k + 1) : ArithmeticFunction ℂ) n =      ((d k : ArithmeticFunction ℂ) * ζ) n by rw [d_succ, natCoe_mul]))]    exact LSeriesSummable_mul ih (LSeriesSummable_zeta_iff.mpr hs)