English
For any a on the unit circle, the zeta has a simple pole at s = 1 with residue 1; equivalently, (s − 1) HurwitzZeta(a, s) tends to 1 when s approaches 1 from any path avoiding s = 1.
Русский
Для любого a на единичной окружности дзета имеет простую полю в s = 1 с остатком 1; эквивалентно, (s − 1) HurwitzZeta(a, s) стремится к 1 при стремлении s к 1 по любому пути, обходя s = 1.
LaTeX
$$$\\displaystyle \\lim_{s\\to 1} (s-1)\\, \\operatorname{HurwitzZeta}(a,s) = 1, \\quad a \\in \\text{UnitAddCircle}. $$$
Lean4
/-- The residue of the Hurwitz zeta function at `s = 1` is `1`. -/
theorem hurwitzZeta_residue_one (a : UnitAddCircle) : Tendsto (fun s ↦ (s - 1) * hurwitzZeta a s) (𝓝[≠] 1) (𝓝 1) :=
by
simp only [hurwitzZeta, mul_add, (by simp : 𝓝 (1 : ℂ) = 𝓝 (1 + (1 - 1) * hurwitzZetaOdd a 1))]
refine (hurwitzZetaEven_residue_one a).add ((Tendsto.mul ?_ ?_).mono_left nhdsWithin_le_nhds)
exacts [tendsto_id.sub_const _, (differentiable_hurwitzZetaOdd a).continuous.tendsto _]
