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), and similarly for completed L-functions.

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.
• completedLFunction χ s: the completed L-function, which for almost all s is equal to LFunction χ s * gammaFactor χ s where gammaFactor χ s is the archimedean Gamma-factor.
• rootNumber: the global root number of the L-series of χ (for χ primitive; junk otherwise).

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.
• LFunction_eq_completed_div_gammaFactor: we have LFunction χ s = completedLFunction χ s / gammaFactor χ s, unless s = 0 and χ is the trivial character modulo 1.
• differentiable_completedLFunction: if χ is nontrivial then completedLFunction χ s is differentiable everywhere.
• IsPrimitive.completedLFunction_one_sub: the functional equation for Dirichlet L-functions, showing that if χ is primitive modulo N, then completedLFunction χ s = N ^ (s - 1 / 2) * rootNumber χ * completedLFunction χ⁻¹ s.

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

• DirichletCharacter.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.deriv_LFunction_eq_deriv_LSeries {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : deriv (LFunction χ) s = deriv (LSeries fun (x : ℕ) => χ ↑x) s

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.

@[simp]

theorem DirichletCharacter.Even.LFunction_neg_two_mul_nat_add_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.Even) (n : ℕ) : LFunction χ (-(2 * (↑n + 1))) = 0

The L-function of an even Dirichlet character vanishes at strictly negative even integers.

@[simp]

theorem DirichletCharacter.Even.LFunction_neg_two_mul_nat {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.Even) (n : ℕ) [NeZero n] : LFunction χ (-(2 * ↑n)) = 0

The L-function of an even Dirichlet character vanishes at strictly negative even integers.

@[simp]

theorem DirichletCharacter.Odd.LFunction_neg_two_mul_nat_sub_one {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.Odd) (n : ℕ) : LFunction χ (-(2 * ↑n) - 1) = 0

The L-function of an odd Dirichlet character vanishes at negative odd integers.

Results on changing levels

theorem DirichletCharacter.LFunction_changeLevel {M N : ℕ} [NeZero M] [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (h : χ ≠ 1 ∨ s ≠ 1) : LFunction ((changeLevel hMN) χ) s = LFunction χ s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

If χ is a Dirichlet character and its level M divides N, then we obtain the L function of χ considered as a Dirichlet character of level N from the L function of χ by multiplying with ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)). (Note that 1 - χ p * p ^ (-s) = 1 when p divides M).

The L-function of the trivial character mod N

@[reducible, inline]

noncomputable abbrev DirichletCharacter.LFunctionTrivChar (N : ℕ) [NeZero N] (s : ℂ) : ℂ

The L-function of the trivial character mod N.

Equations

• DirichletCharacter.LFunctionTrivChar N = DirichletCharacter.LFunction 1

theorem DirichletCharacter.LFunctionTrivChar_eq_mul_riemannZeta {N : ℕ} [NeZero N] {s : ℂ} (hs : s ≠ 1) : LFunctionTrivChar N s = (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * riemannZeta s

The L function of the trivial Dirichlet character mod N is obtained from the Riemann zeta function by multiplying with ∏ p ∈ N.primeFactors, (1 - (p : ℂ) ^ (-s)).

theorem DirichletCharacter.LFunctionTrivChar_residue_one {N : ℕ} [NeZero N] : Filter.Tendsto (fun (s : ℂ) => (s - 1) * LFunctionTrivChar N s) (nhdsWithin 1 {1}ᶜ) (nhds (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)))

The L function of the trivial Dirichlet character mod N has a simple pole with residue ∏ p ∈ N.primeFactors, (1 - p⁻¹) at s = 1.

Completed L-functions and the functional equation

noncomputable def DirichletCharacter.gammaFactor {N : ℕ} (χ : DirichletCharacter ℂ N) (s : ℂ) : ℂ

The Archimedean Gamma factor: Gammaℝ s if χ is even, and Gammaℝ (s + 1) otherwise.

Equations

• χ.gammaFactor s = if χ.Even then s.Gammaℝ else (s + 1).Gammaℝ

theorem DirichletCharacter.Even.gammaFactor_def {N : ℕ} {χ : DirichletCharacter ℂ N} (hχ : χ.Even) (s : ℂ) : χ.gammaFactor s = s.Gammaℝ

theorem DirichletCharacter.Odd.gammaFactor_def {N : ℕ} {χ : DirichletCharacter ℂ N} (hχ : χ.Odd) (s : ℂ) : χ.gammaFactor s = (s + 1).Gammaℝ

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

The completed L-function of a Dirichlet character, almost everywhere equal to LFunction χ s * gammaFactor χ s.

Equations

• DirichletCharacter.completedLFunction χ s = ZMod.completedLFunction (⇑χ) s

theorem DirichletCharacter.completedLFunction_modOne_eq {χ : DirichletCharacter ℂ 1} : completedLFunction χ = completedRiemannZeta

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

theorem DirichletCharacter.differentiableAt_completedLFunction {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) (hs₀ : s ≠ 0 ∨ N ≠ 1) (hs₁ : s ≠ 1 ∨ χ ≠ 1) : DifferentiableAt ℂ (completedLFunction χ) s

The completed L-function of a Dirichlet character is differentiable, with the following exceptions: at s = 1 if χ is the trivial character (to any modulus); and at s = 0 if the modulus is 1. This result is best possible.

Note both χ and s are explicit arguments: we will always be able to infer one or other of them from the hypotheses, but it's not clear which!

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

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

theorem DirichletCharacter.LFunction_eq_completed_div_gammaFactor {N : ℕ} [NeZero N] (χ : DirichletCharacter ℂ N) (s : ℂ) (h : s ≠ 0 ∨ N ≠ 1) : LFunction χ s = completedLFunction χ s / χ.gammaFactor s

Relation between the completed L-function and the usual one. We state it this way around so it holds at the poles of the gamma factor as well.

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

Global root number of χ (for χ primitive; junk otherwise). Defined as gaussSum χ stdAddChar / I ^ a / N ^ (1 / 2), where a = 0 if even, a = 1 if odd. (The factor 1 / I ^ a is the Archimedean root number.) This is a complex number of absolute value 1.

Equations

• χ.rootNumber = (gaussSum χ ZMod.stdAddChar / Complex.I ^ if χ.Even then 0 else 1) / ↑N ^ (1 / 2)

theorem DirichletCharacter.rootNumber_modOne (χ : DirichletCharacter ℂ 1) : χ.rootNumber = 1

The root number of the unique Dirichlet character modulo 1 is 1.

theorem DirichletCharacter.IsPrimitive.completedLFunction_one_sub {N : ℕ} [NeZero N] {χ : DirichletCharacter ℂ N} (hχ : χ.IsPrimitive) (s : ℂ) : completedLFunction χ (1 - s) = ↑N ^ (s - 1 / 2) * χ.rootNumber * completedLFunction χ⁻¹ s

Functional equation for primitive Dirichlet L-functions.

The logarithmic derivative of the L-function of a Dirichlet character

We show that s ↦ -(L' χ s) / L χ s + 1 / (s - 1) is continuous outside the zeros of L χ when χ is a trivial Dirichlet character and that -L' χ / L χ is continuous outside the zeros of L χ when χ is nontrivial.

@[reducible, inline]

noncomputable abbrev DirichletCharacter.LFunctionTrivChar₁ (n : ℕ) [NeZero n] : ℂ → ℂ

The function obtained by "multiplying away" the pole of L χ for a trivial Dirichlet character χ. Its (negative) logarithmic derivative is used to prove Dirichlet's Theorem on primes in arithmetic progression.

Equations

• DirichletCharacter.LFunctionTrivChar₁ n = Function.update (fun (s : ℂ) => (s - 1) * DirichletCharacter.LFunctionTrivChar n s) 1 (∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹))

theorem DirichletCharacter.LFunctionTrivChar₁_apply_one_ne_zero (n : ℕ) [NeZero n] : LFunctionTrivChar₁ n 1 ≠ 0

theorem DirichletCharacter.differentiable_LFunctionTrivChar₁ (n : ℕ) [NeZero n] : Differentiable ℂ (LFunctionTrivChar₁ n)

s ↦ (s - 1) * L χ s is an entire function when χ is a trivial Dirichlet character.

theorem DirichletCharacter.deriv_LFunctionTrivChar₁_apply_of_ne_one (n : ℕ) [NeZero n] {s : ℂ} (hs : s ≠ 1) : deriv (LFunctionTrivChar₁ n) s = (s - 1) * deriv (LFunctionTrivChar n) s + LFunctionTrivChar n s

theorem DirichletCharacter.continuousOn_neg_logDeriv_LFunctionTrivChar₁ (n : ℕ) [NeZero n] : ContinuousOn (fun (s : ℂ) => -deriv (LFunctionTrivChar₁ n) s / LFunctionTrivChar₁ n s) {s : ℂ | s = 1 ∨ LFunctionTrivChar n s ≠ 0}

The negative logarithmic derivative of s ↦ (s - 1) * L χ s for a trivial Dirichlet character χ is continuous away from the zeros of L χ (including at s = 1).

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

The negative logarithmic derivative of the L-function of a nontrivial Dirichlet character is continuous away from the zeros of the L-function.