English
The residue of completedHurwitzZetaEven a s at s = 1 equals 1, uniformly in a on the unit circle.
Русский
Положение вычета completedHurwitzZetaEven a s в точке s = 1 равно 1, независимо от a на единичном круге.
LaTeX
$$$\\forall a:\\text{UnitAddCircle},\\ \\mathrm{Tendsto}\\bigl(s \\mapsto (s-1)\\,\\mathrm{completedHurwitzZetaEven}(a,s),\\ 1\\bigr) = 1.$$$
Lean4
/-- The residue of `completedHurwitzZetaEven a s` at `s = 1` is equal to `1`. -/
theorem completedHurwitzZetaEven_residue_one (a : UnitAddCircle) :
Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1) :=
by
have h1 : Tendsto (fun s : ℂ ↦ (s - ↑(1 / 2 : ℝ)) * _) (𝓝[≠] ↑(1 / 2 : ℝ)) (𝓝 ((1 : ℂ) * (1 : ℂ))) :=
(hurwitzEvenFEPair a).Λ_residue_k
simp only [push_cast, one_mul] at h1
refine (h1.comp <| tendsto_div_two_punctured_nhds 1).congr (fun s ↦ ?_)
rw [completedHurwitzZetaEven, Function.comp_apply, ← sub_div, div_mul_eq_mul_div, mul_div_assoc]
