English
The completed L-function is differentiable at all complex numbers s with the stated pole-exceptions: if χ is trivial, there is a pole at s = 1; if N = 1 there is a pole at s = 0; otherwise it is differentiable everywhere.
Русский
Завершённая L-функция дифференцируема во всех комплексных точках, кроме указанных особенностей: для тривиального χ есть полюс в s = 1; при N = 1 полюс в s = 0; в противном случае дифференцируема повсюду.
LaTeX
$$$\text{DifferentiableAt}(\mathbb{C},\text{completedLFunction}(\chi), s)$ при условиях: либо s ≠ 0 \/ N ≠ 1, и либо s ≠ 1 \/ χ ≠ 1.$$
Lean4
/-- The completed L-function of a Dirichlet character is differentiable, with the following
exceptions: at `s = 1` if `χ` is the trivial character (to any modulus); and at `s = 0` if the
modulus is 1. This result is best possible.
Note both `χ` and `s` are explicit arguments: we will always be able to infer one or other
of them from the hypotheses, but it's not clear which!
-/
theorem differentiableAt_completedLFunction (χ : DirichletCharacter ℂ N) (s : ℂ) (hs₀ : s ≠ 0 ∨ N ≠ 1)
(hs₁ : s ≠ 1 ∨ χ ≠ 1) : DifferentiableAt ℂ (completedLFunction χ) s :=
ZMod.differentiableAt_completedLFunction _ _ (by have := χ.map_zero'; tauto)
(by have := χ.sum_eq_zero_of_ne_one; tauto)
