English
The completed L-function is differentiable everywhere provided Φ(0) = 0 and ∑ Φ(j) = 0.
Русский
Завершенная L-функция дифференцируема во всей плоскости, если Φ(0) = 0 и ∑ Φ(j) = 0.
LaTeX
$$$$\text{Differentiable}_{\mathbb{C}}(\mathrm{completedLFunction}(\Phi))$$$$
Lean4
/-- The completed L-function of a function `ZMod N → ℂ` is differentiable, with the following
exceptions: at `s = 1` if `∑ j, Φ j ≠ 0`; and at `s = 0` if `Φ 0 ≠ 0`.
-/
theorem differentiableAt_completedLFunction (Φ : ZMod N → ℂ) (s : ℂ) (hs₀ : s ≠ 0 ∨ Φ 0 = 0)
(hs₁ : s ≠ 1 ∨ ∑ j, Φ j = 0) : DifferentiableAt ℂ (completedLFunction Φ) s :=
by
simp only [funext (completedLFunction_eq Φ), mul_div_assoc]
-- We know `completedLFunction₀` is differentiable everywhere, so it suffices to show that the
-- correction terms from `completedLFunction_eq` are differentiable at `s`.
refine ((differentiable_completedLFunction₀ _ _).sub ?_).sub ?_
· -- term with `1 / s`
refine .mul (by fun_prop) (hs₀.elim ?_ ?_)
· exact fun h ↦ (differentiableAt_const _).div differentiableAt_id h
· exact fun h ↦ by simp only [h, funext zero_div, differentiableAt_const]
· -- term with `1 / (1 - s)`
refine .mul (by fun_prop) (hs₁.elim ?_ ?_)
· exact fun h ↦ .div (by fun_prop) (by fun_prop) (by rwa [sub_ne_zero, ne_comm])
· exact fun h ↦ by simp only [h, zero_div, differentiableAt_const]
