English
If a lies on the unit circle, the completedCosZeta a is differentiable at s with s ≠ 0, and either s ≠ 1 or a ≠ 0.
Русский
Если a лежит на единичном круге, то function s ↦ completedCosZeta(a,s) дифференцируема в точке s при условии s ≠ 0 и (s ≠ 1 или a ≠ 0).
LaTeX
$$$\\forall a \\in \\text{UnitAddCircle},\\ {s:\\mathbb{C}}\\ (s \\neq 0) \\land (s \\neq 1 \\lor a \\neq 0) \\Rightarrow \\mathrm{DifferentiableAt}_{\\mathbb{C}}(\\mathrm{completedCosZeta}(a), s).$$$
Lean4
theorem differentiableAt_completedCosZeta (a : UnitAddCircle) {s : ℂ} (hs : s ≠ 0) (hs' : s ≠ 1 ∨ a ≠ 0) :
DifferentiableAt ℂ (completedCosZeta a) s :=
by
refine
(((hurwitzEvenFEPair a).symm.differentiableAt_Λ (Or.inl ?_) ?_).comp s (differentiableAt_id.div_const _)).div_const
_
· exact div_ne_zero_iff.mpr ⟨hs, two_ne_zero⟩
· change s / 2 ≠ ↑(1 / 2 : ℝ) ∨ (if a = 0 then 1 else 0) = 0
refine Or.imp (fun h ↦ ?_) (fun ha ↦ ?_) hs'
· simpa [push_cast] using h ∘ (div_left_inj' two_ne_zero).mp
· simpa
