English
The completed L-function is differentiable at s, with exceptions at s = 0 (if Φ(0) ≠ 0) and at s = 1 (if ∑ Φ(j) ≠ 0).
Русский
Завершенная L-функция дифференцируема в точке s, за исключением s = 0 (если Φ(0) ≠ 0) и s = 1 (если ∑ Φ(j) ≠ 0).
LaTeX
$$$$\text{DifferentiableAt}_{\mathbb{C}}(\mathrm{completedLFunction}(\Phi), s) \/\text{ under }(s \neq 0 \lor \Phi(0)=0) \land (s \neq 1 \lor \sum_j \Phi(j)=0).$$$$
Lean4
theorem completedLFunction_eq (Φ : ZMod N → ℂ) (s : ℂ) :
completedLFunction Φ s = completedLFunction₀ Φ s - N ^ (-s) * Φ 0 / s - N ^ (-s) * (∑ j, Φ j) / (1 - s) :=
by
simp only [completedLFunction, completedHurwitzZetaEven_eq, toAddCircle_eq_zero, div_eq_mul_inv, ite_mul, one_mul,
zero_mul, mul_sub, mul_ite, mul_zero, sum_sub_distrib, Fintype.sum_ite_eq', ← sum_mul, completedLFunction₀,
mul_assoc]
abel
