differentiable_completedLFunction

English

If χ is nontrivial, the completed L-function is differentiable everywhere.

Русский

Если χ не тривиален, завершённая L-функция дифференцируема повсюду.

LaTeX

$$$\text{Differentiable}(\text{completedLFunction}(\chi))\quad\text{for } \chi \neq 1$$$

Lean4

/-- The completed L-function of a non-trivial Dirichlet character is differentiable everywhere. -/
theorem differentiable_completedLFunction {χ : DirichletCharacter ℂ N} (hχ : χ ≠ 1) :
    Differentiable ℂ (completedLFunction χ) :=
  by
  refine fun s ↦ differentiableAt_completedLFunction _ _ (Or.inr ?_) (Or.inr hχ)
  exact hχ ∘ level_one' _

Похожие утверждения