English
The Gamma function has a simple pole at 0 with residue 1.
Русский
Функция Гамма имеет простую полюс в нуле с остатком 1.
LaTeX
$$$$ \operatorname{Res}_{s=0} \Gamma(s) = 1. $$$$
Lean4
/-- At `s = 0`, the Gamma function has a simple pole with residue 1. -/
theorem tendsto_self_mul_Gamma_nhds_zero : Tendsto (fun z : ℂ => z * Gamma z) (𝓝[≠] 0) (𝓝 1) :=
by
rw [show 𝓝 (1 : ℂ) = 𝓝 (Gamma (0 + 1)) by simp only [zero_add, Complex.Gamma_one]]
convert
(Tendsto.mono_left _ nhdsWithin_le_nhds).congr'
(eventuallyEq_of_mem self_mem_nhdsWithin Complex.Gamma_add_one) using
1
refine ContinuousAt.comp (g := Gamma) ?_ (continuous_id.add continuous_const).continuousAt
refine (Complex.differentiableAt_Gamma _ fun m => ?_).continuousAt
rw [zero_add, ← ofReal_natCast, ← ofReal_neg, ← ofReal_one, Ne, ofReal_inj]
refine (lt_of_le_of_lt ?_ zero_lt_one).ne'
exact neg_nonpos.mpr (Nat.cast_nonneg _)
