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) and satisfies a functional equation. We also define completed L-functions (given by multiplying the naive L-function by a Gamma-factor), and prove analytic continuation and functional equations for these too, assuming Φ is either even or odd.

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.lean.

Main definitions

• ZMod.LFunction Φ s: the meromorphic continuation of the function ∑ n : ℕ, Φ n * n ^ (-s).
• ZMod.completedLFunction Φ s: the completed L-function, which for almost all s is equal to LFunction Φ s multiplied by an Archimedean Gamma-factor.

Note that ZMod.completedLFunction Φ s is only mathematically well-defined if Φ is either even or odd. Here we extend it to all functions Φ by linearity (but the functional equation only holds if Φ is either even or odd).

Main theorems

Results for non-completed L-functions:

• 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.

Results for completed L-functions:

• ZMod.LFunction_eq_completed_div_gammaFactor_even and LFunction_eq_completed_div_gammaFactor_odd: we have LFunction Φ s = completedLFunction Φ s / Gammaℝ s for Φ even, and LFunction Φ s = completedLFunction Φ s / Gammaℝ (s + 1) for Φ odd. (We formulate it this way around so it is still valid at the poles of the Gamma factor.)
• ZMod.differentiableAt_completedLFunction: ZMod.completedLFunction Φ is differentiable at s ∈ ℂ, unless s = 1 and ∑ j, Φ j ≠ 0, or s = 0 and Φ 0 ≠ 0.
• ZMod.completedLFunction_one_sub_even and ZMod.completedLFunction_one_sub_odd: the functional equation relating completedLFunction Φ (1 - s) to completedLFunction (𝓕 Φ) s.

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 : ℂ) : 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) : 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 ℂ (LFunction Φ) s

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

theorem ZMod.LFunction_residue_one {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) : Filter.Tendsto (fun (s : ℂ) => (s - 1) * 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) : LFunction (fun (k : ZMod N) => stdAddChar (j * k)) s = HurwitzZeta.expZeta (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 : Φ 0 = 0 ∨ s ≠ 1) : LFunction (dft Φ) s = ∑ j : ZMod N, Φ j * HurwitzZeta.expZeta (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' : Φ 0 = 0 ∨ s ≠ 1) : LFunction Φ (1 - s) = ↑N ^ (s - 1) * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * (Complex.exp (↑Real.pi * Complex.I * s / 2) * LFunction (dft Φ) s + Complex.exp (-↑Real.pi * Complex.I * s / 2) * LFunction (dft fun (x : ZMod N) => Φ (-x)) s)

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

theorem ZMod.LFunction_def_even {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Even Φ) (s : ℂ) : LFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * HurwitzZeta.hurwitzZetaEven (toAddCircle j) s

theorem ZMod.LFunction_def_odd {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Odd Φ) (s : ℂ) : LFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * HurwitzZeta.hurwitzZetaOdd (toAddCircle j) s

@[simp]

theorem ZMod.LFunction_apply_zero_of_even {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Even Φ) : LFunction Φ 0 = -Φ 0 / 2

Explicit formula for LFunction Φ 0 when Φ is even.

@[simp]

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

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

@[simp]

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

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

noncomputable def ZMod.completedLFunction {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) (s : ℂ) : ℂ

The completed L-function of a function Φ : ZMod N → ℂ.

This is only mathematically meaningful if Φ is either even, or odd; here we extend this to all Φ by linearity.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ZMod.completedLFunction_zero {N : ℕ} [NeZero N] (s : ℂ) : completedLFunction 0 s = 0

theorem ZMod.completedLFunction_const_mul {N : ℕ} [NeZero N] (a : ℂ) (Φ : ZMod N → ℂ) (s : ℂ) : completedLFunction (fun (j : ZMod N) => a * Φ j) s = a * completedLFunction Φ s

theorem ZMod.completedLFunction_def_even {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Even Φ) (s : ℂ) : completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * HurwitzZeta.completedHurwitzZetaEven (toAddCircle j) s

theorem ZMod.completedLFunction_def_odd {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Odd Φ) (s : ℂ) : completedLFunction Φ s = ↑N ^ (-s) * ∑ j : ZMod N, Φ j * HurwitzZeta.completedHurwitzZetaOdd (toAddCircle j) s

theorem ZMod.completedLFunction_modOne_eq (Φ : ZMod 1 → ℂ) (s : ℂ) : completedLFunction Φ s = Φ 1 * completedRiemannZeta s

The completed L-function of a function ZMod 1 → ℂ is a scalar multiple of the completed Riemann zeta function.

noncomputable def ZMod.completedLFunction₀ {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) (s : ℂ) : ℂ

The completed L-function of a function ZMod N → ℂ, modified by adding multiples of N ^ (-s) / s and N ^ (-s) / (1 - s) to make it entire.

Equations

• One or more equations did not get rendered due to their size.

theorem ZMod.differentiable_completedLFunction₀ {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) : Differentiable ℂ (completedLFunction₀ Φ)

The function completedLFunction₀ Φ is differentiable.

theorem ZMod.completedLFunction_eq {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) (s : ℂ) : completedLFunction Φ s = completedLFunction₀ Φ s - ↑N ^ (-s) * Φ 0 / s - (↑N ^ (-s) * ∑ j : ZMod N, Φ j) / (1 - s)

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

The completed L-function of a function ZMod N → ℂ is differentiable, with the following exceptions: at s = 1 if ∑ j, Φ j ≠ 0; and at s = 0 if Φ 0 ≠ 0.

theorem ZMod.differentiable_completedLFunction {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ₂ : Φ 0 = 0) (hΦ₃ : ∑ j : ZMod N, Φ j = 0) : Differentiable ℂ (completedLFunction Φ)

Special case of differentiableAt_completedLFunction asserting differentiability everywhere under suitable hypotheses.

theorem ZMod.LFunction_eq_completed_div_gammaFactor_even {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Even Φ) (s : ℂ) (hs : s ≠ 0 ∨ Φ 0 = 0) : LFunction Φ s = completedLFunction Φ s / s.Gammaℝ

Relation between the completed L-function and the usual one (even case). We state it this way around so it holds at the poles of the gamma factor as well (except at s = 0, where it is genuinely false if N > 1 and Φ 0 ≠ 0).

theorem ZMod.LFunction_eq_completed_div_gammaFactor_odd {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Odd Φ) (s : ℂ) : LFunction Φ s = completedLFunction Φ s / (s + 1).Gammaℝ

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

theorem ZMod.completedLFunction_one_sub_even {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Even Φ) (s : ℂ) (hs₀ : s ≠ 0 ∨ ∑ j : ZMod N, Φ j = 0) (hs₁ : s ≠ 1 ∨ Φ 0 = 0) : completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * completedLFunction (dft Φ) s

Functional equation for completed L-functions (even case), valid at all points of differentiability.

theorem ZMod.completedLFunction_one_sub_odd {N : ℕ} [NeZero N] {Φ : ZMod N → ℂ} (hΦ : Function.Odd Φ) (s : ℂ) : completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * Complex.I * completedLFunction (dft Φ) s

Functional equation for completed L-functions (odd case), valid for all s.