Theorems · Theorem · number theory

HurwitzZeta.differentiableAt_hurwitzZetaEven

∀ (a : UnitAddCircle) {s : ℂ}, s ≠ 1 → DifferentiableAt ℂ (HurwitzZeta.hurwitzZetaEven a) s

The Hurwitz zeta function is differentiable everywhere except at s = 1. This is true even in the delicate case a = 0 and s = 0 (where the completed zeta has a pole, but this is cancelled out by the Gamma factor).

Defined in

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Cited by

3 results in Mathlib

Foundations

Depth 301 from the axioms · uses propext, Classical.choice, Quot.sound