riemannZeta_abel_integral

theorem riemannZeta_abel_integral (s : ℂ) (hs : 1 < s.re) :    riemannZeta s = zetaAbelContinuationFormula s := by  have hsne : s ≠ 1 := by    intro h    have hre : s.re = 1 := by simp [h]    linarith  set G : ℕ → ℂ := fun N =>    (N : ℂ) ^ (1 - s) / (1 - s) + 1 + 1 / (s - 1)      - s * ∫ u in (1 : ℝ)..N, zetaAbelFractKernel s u  have hEv : ∀ᶠ N in atTop, zetaPartialSum s N = G N :=    (eventually_ge_atTop 1).mono fun N hN => (abel_formula s hsne N hN).trans rfl  have hG_to_zeta := (tendsto_congr' hEv).mp (tendsto_riemannZeta s hs)  have hA : Tendsto (fun N : ℕ => (N : ℂ) ^ (1 - s) / (1 - s)) atTop (𝓝 0) := by    simpa [div_eq_mul_inv, mul_comm] using      (Tendsto.const_mul (1 / (1 - s))        (tendsto_natCast_cpow_zero_of_neg_re (1 - s)          (by rw [Complex.sub_re, Complex.one_re]; linarith)))  have hK : Tendsto (fun _ : ℕ => (1 + 1 / (s - 1) : ℂ)) atTop      (𝓝 (1 + 1 / (s - 1))) := tendsto_const_nhds  have hIntMul := (tendsto_integral_Ioi s hs).const_mul s  set Aseq : ℕ → ℂ := fun N => (N : ℂ) ^ (1 - s) / (1 - s)  set Kseq : ℕ → ℂ := fun _ => (1 + 1 / (s - 1) : ℂ)  set Iseq : ℕ → ℂ := fun N => s * ∫ u in (1 : ℝ)..N, zetaAbelFractKernel s u  have hSum : Tendsto (fun N => Aseq N + Kseq N) atTop (𝓝 (1 + 1 / (s - 1))) := by    simpa using! ((continuous_fst.add continuous_snd).tendsto _).comp (hA.prodMk_nhds hK)  have hG_limit : Tendsto G atTop      (𝓝 ((1 + 1 / (s - 1)) - s * ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u)) := by    have hSub : Tendsto (fun N => Aseq N + Kseq N - Iseq N) atTop        (𝓝 ((1 + 1 / (s - 1)) - s * ∫ u in Ioi (1 : ℝ), zetaAbelFractKernel s u)) := by      simpa [Function.comp_apply, Function.comp_def, sub_eq_add_neg] using        ((continuous_fst.add continuous_snd).tendsto _).comp (hSum.prodMk_nhds hIntMul.neg)    have hGdef : (fun N => Aseq N + Kseq N - Iseq N) = G := by      funext N      simp [Aseq, Kseq, Iseq, G, add_comm, add_left_comm, add_assoc, sub_eq_add_neg]    simpa [hGdef] using hSub  have huniq := tendsto_nhds_unique hG_to_zeta hG_limit  simpa [zetaAbelContinuationFormula, sub_eq_add_neg] using huniq