differentiable_expZeta_of_ne_zero

English

For any a,b ∈ UnitAddCircle, the function s ↦ HurwitzZeta(a,s) − HurwitzZeta(b,s) is differentiable on the complex plane.

Русский

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

LaTeX

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

Lean4

/-- If `a ≠ 0` then the exponential zeta function is analytic everywhere. -/
theorem differentiable_expZeta_of_ne_zero {a : UnitAddCircle} (ha : a ≠ 0) : Differentiable ℂ (expZeta a) :=
  (differentiableAt_expZeta a · (Or.inr ha))

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