English
The residue at s = 0 for completedHurwitzZetaEven a s is -1 if a = 0, and 0 otherwise.
Русский
Положение вычета в точке s = 0 для completedHurwitzZetaEven a s равно -1, если a = 0, и 0 в противном случае.
LaTeX
$$$\\forall a:\\text{UnitAddCircle},\\ \\mathrm{Tendsto}\\bigl(s \\mapsto s\\,\\mathrm{completedHurwitzZetaEven}(a,s),\\ 0\\bigr) = \\begin{cases}-1,& a=0\\\\ 0,& a\\neq 0\\end{cases}.$$$
Lean4
/-- The residue of `completedHurwitzZetaEven a s` at `s = 0` is equal to `-1` if `a = 0`, and `0`
otherwise. -/
theorem completedHurwitzZetaEven_residue_zero (a : UnitAddCircle) :
Tendsto (fun s ↦ s * completedHurwitzZetaEven a s) (𝓝[≠] 0) (𝓝 (if a = 0 then -1 else 0)) :=
by
have h1 : Tendsto (fun s : ℂ ↦ s * _) (𝓝[≠] 0) (𝓝 (-(if a = 0 then 1 else 0))) := (hurwitzEvenFEPair a).Λ_residue_zero
have : -(if a = 0 then (1 : ℂ) else 0) = (if a = 0 then -1 else 0) := by { split_ifs <;> simp
}
simp only [this, push_cast] at h1
refine (h1.comp <| zero_div (2 : ℂ) ▸ (tendsto_div_two_punctured_nhds 0)).congr (fun s ↦ ?_)
simp [completedHurwitzZetaEven, div_mul_eq_mul_div, mul_div_assoc]
