theorem DirichletCharacter.lFunction_entire_of_ne_one {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ ≠ 1) : Differentiable ℂ (LFunction χ)

A nonprincipal Dirichlet L-function is entire in the differentiability API.

theorem DirichletCharacter.completedLFunction_entire_of_ne_one {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ ≠ 1) : Differentiable ℂ (completedLFunction χ)

The completed L-function is entire for a nonprincipal character.

theorem DirichletCharacter.LSeries_twist_vonMangoldt_eq_neg_logDeriv_LFunction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) {s : ℂ} (hs : 1 < s.re) : LSeries ((fun (n : ℕ) => χ ↑n) * fun (n : ℕ) => ↑(ArithmeticFunction.vonMangoldt n)) s = -deriv (LFunction χ) s / LFunction χ s

In the half-plane of absolute convergence, the negative logarithmic derivative is the L-series of the von Mangoldt twist.

theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunction {q : ℕ} [NeZero q] {χ : DirichletCharacter ℂ q} (hχ : χ ≠ 1) : ContinuousOn (fun (s : ℂ) => -deriv (LFunction χ) s / LFunction χ s) {s : ℂ | LFunction χ s ≠ 0}

The negative logarithmic derivative is continuous wherever a nonprincipal Dirichlet L-function is nonzero.