Analytic continuation of Dirichlet L-functions

We show that if χ is a Dirichlet character ZMod N → ℂ, for a positive integer N, then the L-series of χ has analytic continuation (away from a pole at s = 1 if χ is trivial).

All definitions and theorems are in the DirichletCharacter namespace.

Main definitions

• LFunction χ s: the L-function, defined as a linear combination of Hurwitz zeta functions.

Main theorems

• LFunction_eq_LSeries: if 1 < re s then the LFunction coincides with the naive LSeries.
• differentiable_LFunction: if χ is nontrivial then LFunction χ s is differentiable everywhere.

noncomputable def DirichletCharacter.LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂ

The unique meromorphic function ℂ → ℂ which agrees with ∑' n : ℕ, χ n / n ^ s wherever the latter is convergent. This is constructed as a linear combination of Hurwitz zeta functions.

Note that this is not the same as LSeries χ: they agree in the convergence range, but LSeries χ s is defined to be 0 if re s ≤ 1.

Equations

• χ.LFunction s = ZMod.LFunction (⇑χ) s

@[simp]

theorem DirichletCharacter.LFunction_modOne_eq {χ : DirichletCharacter ℂ 1} : χ.LFunction = riemannZeta

The L-function of the (unique) Dirichlet character mod 1 is the Riemann zeta function. (Compare DirichletCharacter.LSeries_modOne_eq.)

theorem DirichletCharacter.LFunction_eq_LSeries {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : χ.LFunction s = LSeries (fun (x : ℕ) => χ ↑x) s

For 1 < re s the L-function of a Dirichlet character agrees with the sum of the naive Dirichlet series.

theorem DirichletCharacter.differentiableAt_LFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) (hs : s ≠ 1 ∨ χ ≠ 1) : DifferentiableAt ℂ χ.LFunction s

The L-function of a Dirichlet character is differentiable, except at s = 1 if the character is trivial.

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

The L-function of a non-trivial Dirichlet character is differentiable everywhere.