English
As s approaches 0 (s ≠ 0), the product s · Γℝ(s) tends to 2.
Русский
При приближении к нулю (s ≠ 0) произведение s · Γℝ(s) стремится к 2.
LaTeX
$$$$ \\lim_{s \\to 0,\, s \\neq 0} s\\,\\Gamma_{\\mathbb{R}}(s) = 2. $$$$
Lean4
theorem Gammaℝ_residue_zero : Tendsto (fun s ↦ s * Gammaℝ s) (𝓝[≠] 0) (𝓝 2) :=
by
have h : Tendsto (fun z : ℂ ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1) :=
by
refine tendsto_self_mul_Gamma_nhds_zero.comp ?_
rw [tendsto_nhdsWithin_iff, (by simp : 𝓝 (0 : ℂ) = 𝓝 (0 / 2))]
exact
⟨(tendsto_id.div_const _).mono_left nhdsWithin_le_nhds,
eventually_of_mem self_mem_nhdsWithin fun x hx ↦ div_ne_zero hx two_ne_zero⟩
have h' : Tendsto (fun s : ℂ ↦ 2 * (π : ℂ) ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2) :=
by
rw [(by simp : 𝓝 2 = 𝓝 (2 * (π : ℂ) ^ (-(0 : ℂ) / 2)))]
refine Tendsto.mono_left (ContinuousAt.tendsto ?_) nhdsWithin_le_nhds
exact
continuousAt_const.mul
((continuousAt_const_cpow (ofReal_ne_zero.mpr pi_ne_zero)).comp (continuousAt_id.neg.div_const _))
convert mul_one (2 : ℂ) ▸ (h'.mul h) using 2 with z
rw [Gammaℝ]
ring_nf
