English
The difference between two completed even Hurwitz zeta functions is differentiable at s = 1.
Русский
Разность двух завершённых чётных zeta-функций Хёрвитца является дифференцируемой в точке s = 1.
LaTeX
$$$\\forall a,b \\in \\text{UnitAddCircle},\\ \\mathrm{DifferentiableAt}_{\\mathbb{C}}\\bigl(\\lambda s.\\ \\mathrm{completedHurwitzZetaEven}(a,s) - \\mathrm{completedHurwitzZetaEven}(b,s)\\bigr)\\,\\text{at } s=1$$$
Lean4
/-- The difference of two completed even Hurwitz zeta functions is differentiable at `s = 1`. -/
theorem differentiableAt_one_completedHurwitzZetaEven_sub_completedHurwitzZetaEven (a b : UnitAddCircle) :
DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven a s - completedHurwitzZetaEven b s) 1 :=
by
have (s : _) :
completedHurwitzZetaEven a s - completedHurwitzZetaEven b s =
completedHurwitzZetaEven₀ a s - completedHurwitzZetaEven₀ b s -
((if a = 0 then 1 else 0) - (if b = 0 then 1 else 0)) / s :=
by
simp_rw [completedHurwitzZetaEven_eq, sub_div]
abel
rw [funext this]
refine .sub ?_ <| (differentiable_const _ _).div (differentiable_id _) one_ne_zero
apply DifferentiableAt.sub <;> apply differentiable_completedHurwitzZetaEven₀
