English
The cosine zeta function is differentiable at every point s in the complex plane except possibly at s=1 when a=0; more precisely, for any a and s with s ≠ 1 or a ≠ 0, cosZeta is differentiable at s.
Русский
Косинусная зета дифференцируема во всех точках комплексной плоскости, за исключением s=1, если a=0; в общем случае для любых a и s с s ≠ 1 или a ≠ 0 функция дифференцируема в s.
LaTeX
$$$$\\text{If } s \\neq 1 \\lor a \\neq 0, \\quad \\frac{d}{ds}\\cosZeta(a)(s) \\text{ exists.}$$$$
Lean4
/-- The cosine zeta function is differentiable everywhere, except at `s = 1` if `a = 0`. -/
theorem differentiableAt_cosZeta (a : UnitAddCircle) {s : ℂ} (hs' : s ≠ 1 ∨ a ≠ 0) : DifferentiableAt ℂ (cosZeta a) s :=
by
rcases ne_or_eq s 1 with hs' | rfl
·
exact
differentiableAt_update_of_residue (fun _ ht ht' ↦ differentiableAt_completedCosZeta a ht (Or.inl ht'))
(completedCosZeta_residue_zero a) s hs'
· apply
((differentiableAt_completedCosZeta a one_ne_zero hs').fun_mul
(differentiable_Gammaℝ_inv.differentiableAt)).congr_of_eventuallyEq
filter_upwards [isOpen_compl_singleton.mem_nhds one_ne_zero] with x hx
rw [cosZeta, Function.update_of_ne hx, div_eq_mul_inv]
