differentiableAt_hurwitzZeta_sub_one_div

English

For a on the unit circle, the function s ↦ HurwitzZeta(a,s) − 1/((s−1)Γ(s)) is differentiable at s = 1; equivalently, removing the simple pole yields an analytic function at 1.

Русский

Для a на единичной окружности функция s ↦ HurwitzZeta(a,s) − 1/((s−1)Γ(s)) дифференцируема в точке s = 1; то есть удаление простой полюсы даёт аналитическую функцию в 1.

LaTeX

$$$\\displaystyle \\text{DifferentiableAt}_{\\mathbb{C}}\\left( s \\mapsto \\operatorname{HurwitzZeta}(a,s) - \\frac{1}{(s-1) \\Gamma(s)}\\right)\\big|_{s=1}. $$$

Lean4

theorem differentiableAt_hurwitzZeta_sub_one_div (a : UnitAddCircle) :
    DifferentiableAt ℂ (fun s ↦ hurwitzZeta a s - 1 / (s - 1) / Gammaℝ s) 1 :=
  by
  simp only [hurwitzZeta, add_sub_right_comm]
  exact (differentiableAt_hurwitzZetaEven_sub_one_div a).add (differentiable_hurwitzZetaOdd a 1)

Похожие утверждения