tendsto_riemannZeta_sub_one_div_Gammaℝ

English

Let ζ be the Riemann zeta function and Γ the Gamma function. Then as s approaches 1 with s ≠ 1, ζ(s) − 1/(Γ(s)(s−1)) tends to (γ − log(4π))/2.

Русский

Пусть ζ — дзета-функция Римана, а Γ — гамма-функция. Тогда при s→1, s ≠ 1, ζ(s) − 1/(Γ(s)(s−1)) стремится к (γ − log(4π))/2.

LaTeX

$$$$ \displaystyle \lim_{\substack{s \to 1 \\ s \neq 1}} \left( \zeta(s) - \frac{1}{\Gamma(s)(s-1)} \right) = \frac{\gamma - \log(4\pi)}{2}. $$$$

Lean4

theorem tendsto_riemannZeta_sub_one_div_Gammaℝ :
    Tendsto (fun s ↦ riemannZeta s - 1 / Gammaℝ s / (s - 1)) (𝓝[≠] 1) (𝓝 ((γ - Complex.log (4 * ↑π)) / 2)) :=
  by
  have := tendsto_riemannZeta_sub_one_div.add tendsto_Gamma_term_aux
  simp_rw [sub_add_sub_cancel] at this
  convert this using 2
  ring_nf

Похожие утверждения