differentiableAt_hurwitzZeta — Mathlib

English

The Hurwitz zeta function is differentiable at s whenever s ≠ 1.

Русский

Функция Хёрвитц-зета дифференцируема при любом s, отличном от 1.

LaTeX

$$$\text{DifferentiableAt}(\text{HurwitzZeta}(a), s)\quad\text{for } s \neq 1$$$

Lean4

/-- The Hurwitz zeta function is differentiable away from `s = 1`. -/
theorem differentiableAt_hurwitzZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 1) : DifferentiableAt ℂ (hurwitzZeta a) s :=
  (differentiableAt_hurwitzZetaEven a hs).add (differentiable_hurwitzZetaOdd a s)

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