English
The residue of hurwitzZetaEven at s = 1 is 1 (alternative formulation).
Русский
Остаток 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
theorem hurwitzZetaEven_residue_one (a : UnitAddCircle) :
Tendsto (fun s ↦ (s - 1) * hurwitzZetaEven a s) (𝓝[≠] 1) (𝓝 1) :=
by
have : Tendsto (fun s ↦ (s - 1) * completedHurwitzZetaEven a s / Gammaℝ s) (𝓝[≠] 1) (𝓝 1) := by
simpa only [Gammaℝ_one, inv_one, mul_one] using
(completedHurwitzZetaEven_residue_one a).mul <|
(differentiable_Gammaℝ_inv.continuous.tendsto _).mono_left nhdsWithin_le_nhds
refine this.congr' ?_
filter_upwards [eventually_ne_nhdsWithin one_ne_zero] with s hs
simp [hurwitzZetaEven_def_of_ne_or_ne (Or.inr hs), mul_div_assoc]
