English
For a function Φ: ZMod N → C and a complex number s, if s ≠ 1 or the average of Φ is zero, then LFunction Φ is differentiable at s.
Русский
Пусть Φ: ZMod N → ℂ и s ∈ ℂ. Если s ≠ 1 или среднее значение Φ равно нулю, то LFunction Φ дифференцируема в точке s.
LaTeX
$$$$\text{DifferentiableAt}_{\mathbb{C}}(L(\Phi, \cdot), s) \quad\text{if } s \neq 1 \;\text{or } \sum_j \Phi(j) = 0.$$$$
Lean4
theorem differentiableAt_LFunction (Φ : ZMod N → ℂ) (s : ℂ) (hs : s ≠ 1 ∨ ∑ j, Φ j = 0) :
DifferentiableAt ℂ (LFunction Φ) s := by
refine .mul (by fun_prop) ?_
rcases ne_or_eq s 1 with hs' | rfl
· exact .fun_sum fun j _ ↦ (differentiableAt_hurwitzZeta _ hs').const_mul _
· have :=
DifferentiableAt.fun_sum (u := univ) fun j _ ↦
(differentiableAt_hurwitzZeta_sub_one_div (toAddCircle j)).const_mul (Φ j)
simpa only [mul_sub, sum_sub_distrib, ← sum_mul, hs.neg_resolve_left rfl, zero_mul, sub_zero]
