ZetaPartialSum.tendsto_riemannZeta

theorem tendsto_riemannZeta (s : ℂ) (hs : 1 < s.re) :    Tendsto (fun N : ℕ => zetaPartialSum s N) atTop (𝓝 (riemannZeta s)) := by  set g : ℕ → ℂ := fun n => if n = 0 then 0 else (n : ℂ) ^ (-s)  set h : ℕ → ℂ := fun n => (n + 1 : ℂ) ^ (-s)  have hsne : s ≠ 0 := by    intro h0    have : (0 : ℝ) < s.re := lt_trans (show (0 : ℝ) < 1 by norm_num) hs    simpa [h0] using ne_of_gt this  have hgSumm : Summable g := by    simpa [g, one_div_natCast_cpow_eq_ite_cpow_neg s hsne] using      (Complex.summable_one_div_nat_cpow (p := s)).2 hs  have hhSumm : Summable h := by    have : Summable (fun n => g (n + 1)) := (summable_nat_add_iff (f := g) (k := 1)).2 hgSumm    simpa [Function.comp_apply, h, g] using this  have hg0 : g 0 = 0 := by simp [g]  have h_tsum_eq : (∑' n, h n) = ∑' n, g n := by    have : (∑' n, g n) = ∑' n, g (n + 1) := by simpa [hg0, add_comm] using Summable.tsum_eq_zero_add hgSumm    simpa [h, g] using this.symm  have hzeta : riemannZeta s = ∑' n, g n := by    simpa [g, one_div_natCast_cpow_eq_ite_cpow_neg s hsne] using      zeta_eq_tsum_one_div_nat_cpow (s := s) hs  simpa [zetaPartialSum, h, h_tsum_eq.trans hzeta.symm] using Summable.tendsto_sum_tsum_nat hhSumm