English
As s → 1, HurwitzZeta(a,s) − 1/((s−1)Γ(s)) tends to HurwitzZeta(a,1); i.e., the regularized value at 1 matches the limit from above.
Русский
При приближении s к 1 잘 HurwitzZeta(a,s) − 1/((s−1)Γ(s)) стремится к HurwitzZeta(a,1); т.е. регуляризованное значение в 1 совпадает с пределом.
LaTeX
$$$\\displaystyle \\lim_{s \\to 1} \\left( \\operatorname{HurwitzZeta}(a,s) - \\frac{1}{(s-1)\\Gamma(s)} \\right) = \\operatorname{HurwitzZeta}(a,1).$$$
Lean4
/-- Expression for `hurwitzZeta a 1` as a limit. (Mathematically `hurwitzZeta a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is). -/
theorem tendsto_hurwitzZeta_sub_one_div_nhds_one (a : UnitAddCircle) :
Tendsto (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) (𝓝 1) (𝓝 (hurwitzZeta a 1)) :=
by
simp only [hurwitzZeta, add_sub_right_comm]
refine (tendsto_hurwitzZetaEven_sub_one_div_nhds_one a).add (differentiable_hurwitzZetaOdd a 1).continuousAt.tendsto
