English
The residue of hurwitzZetaEven at s = 1 is 1, in the punctured neighbourhood.
Русский
Остаток hurwitzZetaEven в точке s = 1 равен 1 в проколотом окрестном множестве.
LaTeX
$$$\\forall a:\\text{UnitAddCircle},\\ \\mathrm{Tendsto}\\bigl((s-1)\\mathrm{hurwitzZetaEven}(a,s),\\, \\mathcal{N}_{\\neq 0},\\, \\mathcal{N}(1)\\bigr) = 1.$$$
Lean4
/-- The Hurwitz zeta function is differentiable everywhere except at `s = 1`. This is true
even in the delicate case `a = 0` and `s = 0` (where the completed zeta has a pole, but this is
cancelled out by the Gamma factor). -/
theorem differentiableAt_hurwitzZetaEven (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1) :
DifferentiableAt ℂ (hurwitzZetaEven a) s :=
by
have :=
differentiableAt_update_of_residue (fun t ht ht' ↦ differentiableAt_completedHurwitzZetaEven a (Or.inl ht) ht')
(completedHurwitzZetaEven_residue_zero a) s hs'
simp_rw [div_eq_mul_inv, ite_mul, zero_mul, ← div_eq_mul_inv] at this
exact this
