English
The function s ↦ hurwitzZetaEven a s minus 1/(s-1)/Gamma(s) is differentiable at s = 1, for all a.
Русский
Функция s ↦ hurwitzZetaEven a s − 1/(s−1)/Γ(s) дифференцируема в точке s = 1 для всех a.
LaTeX
$$$\\forall a:\\mathbb{R},\\ DifferentiableAt_{\\mathbb{C}}\\left( s \\mapsto \\mathrm{hurwitzZetaEven}(a,s) - \\frac{1}{s-1}\\cdot\\frac{1}{\\Gamma(s)}\\right)\\bigg|_{s=1}.$$$
Lean4
theorem differentiableAt_hurwitzZetaEven_sub_one_div (a : UnitAddCircle) :
DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - 1 / (s - 1) / Gammaℝ s) 1 :=
by
suffices DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s / Gammaℝ s - 1 / (s - 1) / Gammaℝ s) 1
by
apply this.congr_of_eventuallyEq
filter_upwards [eventually_ne_nhds one_ne_zero] with x hx
rw [hurwitzZetaEven, Function.update_of_ne hx]
simp_rw [← sub_div, div_eq_mul_inv _ (Gammaℝ _)]
refine DifferentiableAt.mul ?_ differentiable_Gammaℝ_inv.differentiableAt
simp_rw [completedHurwitzZetaEven_eq, sub_sub, add_assoc]
conv => enter [2, s, 2]; rw [← neg_sub, div_neg, neg_add_cancel, add_zero]
exact
(differentiable_completedHurwitzZetaEven₀ a _).sub <| (differentiableAt_const _).div differentiableAt_id one_ne_zero
