Kadiri.logDeriv_completedZetaFactor

theorem logDeriv_completedZetaFactor (s : ℂ)    (hs1 : s ≠ 1)    (hΓdiff : ∀ m : ℕ, s / 2 + 1 ≠ -m)    (hΓ : zetaGammaFactor s ≠ 0)    (hζ : riemannZeta s ≠ 0) :    logDeriv completedZetaFactor s =      1 / (s - 1)      - (1 / 2 : ℂ) * Real.log Real.pi      + (1 / 2 : ℂ) * digamma (s / 2 + 1)      + deriv riemannZeta s / riemannZeta s := by  have hpole : zetaPoleFactor s ≠ 0 := by    simp [zetaPoleFactor, sub_ne_zero, hs1]  have hpi : zetaPiFactor s ≠ 0 := by    simp [zetaPiFactor]  have hpole_diff : DifferentiableAt ℂ zetaPoleFactor s := by    unfold zetaPoleFactor    fun_prop  have hpi_diff : DifferentiableAt ℂ zetaPiFactor s := by    unfold zetaPiFactor    fun_prop  have hgamma_diff : DifferentiableAt ℂ zetaGammaFactor s := by    unfold zetaGammaFactor    exact (differentiableAt_Gamma _ hΓdiff).comp s (by fun_prop)  have hzeta_diff : DifferentiableAt ℂ riemannZeta s :=    differentiableAt_riemannZeta hs1  unfold completedZetaFactor  rw [logDeriv_mul]  · rw [logDeriv_mul]    · rw [logDeriv_mul]      · rw [logDeriv_zetaPoleFactor, logDeriv_zetaPiFactor,          logDeriv_zetaGammaFactor s hΓdiff, logDeriv_apply]        ring      · exact hpole      · exact hpi      · exact hpole_diff      · exact hpi_diff    · exact mul_ne_zero hpole hpi    · exact hΓ    · exact hpole_diff.mul hpi_diff    · exact hgamma_diff  · exact mul_ne_zero (mul_ne_zero hpole hpi) hΓ  · exact hζ  · exact (hpole_diff.mul hpi_diff).mul hgamma_diff  · exact hzeta_diff