differentiable_hurwitzZeta_sub_hurwitzZeta

English

For any a,b on the unit circle, the function s ↦ HurwitzZeta(a,s) − HurwitzZeta(b,s) is differentiable everywhere in the complex plane.

Русский

Для любых a,b на единичной окружности функция s ↦ HurwitzZeta(a,s) − HurwitzZeta(b,s) дифференцируема во всей комплексной плоскости.

LaTeX

$$$\\displaystyle \\forall a,b \\in \\mathrm{UnitAddCircle},\\ \\text{Differentiable}_{\\mathbb{C}}\\bigl(s \\mapsto \\operatorname{HurwitzZeta}(a,s) - \\operatorname{HurwitzZeta}(b,s)\\bigr).$$$

Lean4

/-- The difference of two Hurwitz zeta functions is differentiable everywhere. -/
theorem differentiable_hurwitzZeta_sub_hurwitzZeta (a b : UnitAddCircle) :
    Differentiable ℂ (fun s ↦ hurwitzZeta a s - hurwitzZeta b s) :=
  by
  simp only [hurwitzZeta, add_sub_add_comm]
  refine (differentiable_hurwitzZetaEven_sub_hurwitzZetaEven a b).add (.sub ?_ ?_)
  all_goals apply differentiable_hurwitzZetaOdd

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