English
Let a lie on the unit circle. Then the map s ↦ completedHurwitzZetaEven a s is differentiable at every complex s with s ≠ 1, provided either s ≠ 0 or a ≠ 0 (in particular it is differentiable away from s = 1, and also differentiable at s = 0 when a ≠ 0).
Русский
Пусть a принадлежит единичному кругу. Тогда отображение s ↦ completedHurwitzZetaEven a s дифференцируемо в комплексной области для каждого s с s ≠ 1, при условии s ≠ 0 или a ≠ 0 (в частности, дифференцируемо вне точки s = 1 и также в точке s = 0, если a ≠ 0).
LaTeX
$$$\\forall a \\in \\text{UnitAddCircle},\\ \\forall s \\in \\mathbb{C},\\ (s \\neq 1) \\land (s \\neq 0 \\lor a \\neq 0) \\Rightarrow \\mathrm{DifferentiableAt}_{\\mathbb{C}}(\\mathrm{completedHurwitzZetaEven}(a), s).$$$
Lean4
/-- The even Hurwitz completed zeta is differentiable away from `s = 0` and `s = 1` (and also at
`s = 0` if `a ≠ 0`)
-/
theorem differentiableAt_completedHurwitzZetaEven (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0 ∨ a ≠ 0) (hs' : s ≠ 1) :
DifferentiableAt ℂ (completedHurwitzZetaEven a) s :=
by
refine
(((hurwitzEvenFEPair a).differentiableAt_Λ ?_ (Or.inl ?_)).comp s (differentiableAt_id.div_const _)).div_const _
· rcases hs with h | h <;> simp [hurwitzEvenFEPair, h]
· change s / 2 ≠ ↑(1 / 2 : ℝ)
rw [ofReal_div, ofReal_one, ofReal_ofNat]
exact hs' ∘ (div_left_inj' two_ne_zero).mp
