continuousOn_neg_logDeriv_LFunction_of_nontriv

English

The completed L-function is differentiable everywhere for a nontrivial Dirichlet character χ.

Русский

Для непустого χ функция завершённой L имеет дифференцируемость во всей комплексной плоскости.

LaTeX

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

Lean4

/-- The negative logarithmic derivative of the L-function of a nontrivial Dirichlet character
is continuous away from the zeros of the L-function. -/
theorem continuousOn_neg_logDeriv_LFunction_of_nontriv (hχ : χ ≠ 1) :
    ContinuousOn (fun s ↦ -deriv (LFunction χ) s / LFunction χ s) {s | LFunction χ s ≠ 0} :=
  by
  have h := differentiable_LFunction hχ
  simpa [neg_div] using
    ((h.contDiff.continuous_deriv le_rfl).continuousOn.div h.continuous.continuousOn fun _ hw ↦ hw).neg

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