English
Let Γ denote the complex Gamma function. Then the limit as s approaches 1, with s ≠ 1, of the expression 1/(s−1) − 1/(Γ(s)(s−1)) equals −(γ + log(4π))/2, where γ is the Euler–Mascheroni constant.
Русский
Пусть Γ обозначает комплексную гамма-функцию. Тогда предел при s→1, s ≠ 1, выражения 1/(s−1) − 1/(Γ(s)(s−1)) равен −(γ + log(4π))/2, где γ — константа Эйлера-Маскерони.
LaTeX
$$$$ \displaystyle \lim_{\substack{s \to 1 \\ s \neq 1}} \left( \frac{1}{s-1} - \frac{1}{\Gamma(s)(s-1)} \right) = -\frac{\gamma + \log(4\pi)}{2}.$$$$
Lean4
theorem tendsto_Gamma_term_aux :
Tendsto (fun s ↦ 1 / (s - 1) - 1 / Gammaℝ s / (s - 1)) (𝓝[≠] 1) (𝓝 (-(γ + Complex.log (4 * ↑π)) / 2)) :=
by
have h := hasDerivAt_Gammaℝ_one
rw [hasDerivAt_iff_tendsto_slope, slope_fun_def_field, Gammaℝ_one] at h
have :=
h.div (hasDerivAt_Gammaℝ_one.continuousAt.tendsto.mono_left nhdsWithin_le_nhds) (Gammaℝ_one.trans_ne one_ne_zero)
rw [Gammaℝ_one, div_one] at this
refine this.congr' ?_
have : {z | 0 < re z} ∈ 𝓝 (1 : ℂ) :=
by
apply (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds
simp only [mem_preimage, one_re, mem_Ioi, zero_lt_one]
rw [EventuallyEq, eventually_nhdsWithin_iff]
filter_upwards [this] with a ha _
rw [Pi.div_apply, ← sub_div, div_right_comm, sub_div' (Gammaℝ_ne_zero_of_re_pos ha), one_mul]
