L-series of functions on ZMod N

We show that if N is a positive integer and Φ : ZMod N → ℂ, then the L-series of Φ has analytic continuation (away from a pole at s = 1 if ∑ j, Φ j ≠ 0).

The most familiar case is when Φ is a Dirichlet character, but the results here are valid for general functions; for the specific case of Dirichlet characters see Mathlib.NumberTheory.LSeries.DirichletContinuation.

Main definitions

• ZMod.LFunction Φ s: the meromorphic continuation of the function ∑ n : ℕ, Φ n * n ^ (-s).

Main theorems

• ZMod.LFunction_eq_LSeries: if 1 < re s then the LFunction coincides with the naive LSeries.
• ZMod.differentiableAt_LFunction: ZMod.LFunction Φ is differentiable at s ∈ ℂ if either s ≠ 1 or ∑ j, Φ j = 0.
• ZMod.LFunction_one_sub: the functional equation relating LFunction Φ (1 - s) to LFunction (𝓕 Φ) s, where 𝓕 is the Fourier transform.

theorem ZMod.LSeriesSummable_of_one_lt_re {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ} (hs : 1 < s.re) : LSeriesSummable (fun (x : ℕ) => Φ ↑x) s

If Φ is a periodic function, then the L-series of Φ converges for 1 < re s.

noncomputable def ZMod.LFunction {N : ℕ} [NeZero N] (Φ : ZMod 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

• ZMod.LFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * HurwitzZeta.hurwitzZeta (ZMod.toAddCircle j) s

theorem ZMod.LFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) : ZMod.LFunction Φ s = Φ 0 * riemannZeta s

The L-function of a function on ZMod 1 is a scalar multiple of the Riemann zeta function.

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

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

theorem ZMod.differentiableAt_LFunction {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) (s : ℂ) (hs : s ≠ 1 ∨ ∑ j : ZMod N, Φ j = 0) : DifferentiableAt ℂ (ZMod.LFunction Φ) s

theorem ZMod.differentiable_LFunction_of_sum_zero {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : ∑ j : ZMod N, Φ j = 0) : Differentiable ℂ (ZMod.LFunction Φ)

theorem ZMod.LFunction_residue_one {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * ZMod.LFunction Φ s) (nhdsWithin 1 {1}ᶜ) (nhds (∑ j : ZMod N, Φ j / ↑N))

The L-function of Φ has a residue at s = 1 equal to the average value of Φ.

theorem ZMod.LFunction_stdAddChar_eq_expZeta {N : ℕ} [NeZero N] (j : ZMod N) (s : ℂ) (hjs : j ≠ 0 ∨ s ≠ 1) : ZMod.LFunction (fun (k : ZMod N) => ZMod.stdAddChar (j * k)) s = HurwitzZeta.expZeta (ZMod.toAddCircle j) s

The LFunction of the function x ↦ e (j * x), where e : ZMod N → ℂ is the standard additive character, is expZeta (j / N).

Note this is not at all obvious from the definitions, and we prove it by analytic continuation from the convergence range.

theorem ZMod.LFunction_dft {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ} (hs : s ≠ 1) : ZMod.LFunction (ZMod.dft Φ) s = ∑ j : ZMod N, Φ j * HurwitzZeta.expZeta (ZMod.toAddCircle (-j)) s

Explicit formula for the L-function of 𝓕 Φ, where 𝓕 is the discrete Fourier transform.

theorem ZMod.LFunction_one_sub {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) (hs' : s ≠ 1) : ZMod.LFunction Φ (1 - s) = ↑N ^ (s - 1) * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * (Complex.exp (↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft Φ) s + Complex.exp (-↑Real.pi * Complex.I * s / 2) * ZMod.LFunction (ZMod.dft fun (x : ZMod N) => Φ (-x)) s)

Functional equation for ZMod L-functions, in terms of discrete Fourier transform.