Documentation

Mathlib.NumberTheory.LSeries.ZMod

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.

Main definitions #

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:

Results for completed L-functions:

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
Instances For
    theorem ZMod.LFunction_modOne_eq (Φ : ZMod 1) (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) :
    theorem ZMod.differentiable_LFunction_of_sum_zero {N : } [NeZero N] {Φ : ZMod N} (hΦ : j : ZMod N, Φ j = 0) :
    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 : Φ 0 = 0 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' : Φ 0 = 0 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.

    theorem ZMod.LFunction_def_even {N : } [NeZero N] {Φ : ZMod N} (hΦ : Function.Even Φ) (s : ) :
    ZMod.LFunction Φ s = N ^ (-s) * j : ZMod N, Φ j * HurwitzZeta.hurwitzZetaEven (ZMod.toAddCircle j) s
    theorem ZMod.LFunction_def_odd {N : } [NeZero N] {Φ : ZMod N} (hΦ : Function.Odd Φ) (s : ) :
    ZMod.LFunction Φ s = N ^ (-s) * j : ZMod N, Φ j * HurwitzZeta.hurwitzZetaOdd (ZMod.toAddCircle j) s
    @[simp]
    theorem ZMod.LFunction_apply_zero_of_even {N : } [NeZero N] {Φ : ZMod N} (hΦ : Function.Even Φ) :
    ZMod.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 : ) :
    ZMod.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 : ) :
    ZMod.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.
    Instances For
      theorem ZMod.completedLFunction_def_even {N : } [NeZero N] {Φ : ZMod N} (hΦ : Function.Even Φ) (s : ) :
      ZMod.completedLFunction Φ s = N ^ (-s) * j : ZMod N, Φ j * HurwitzZeta.completedHurwitzZetaEven (ZMod.toAddCircle j) s
      theorem ZMod.completedLFunction_def_odd {N : } [NeZero N] {Φ : ZMod N} (hΦ : Function.Odd Φ) (s : ) :
      ZMod.completedLFunction Φ s = N ^ (-s) * j : ZMod N, Φ j * HurwitzZeta.completedHurwitzZetaOdd (ZMod.toAddCircle j) 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.
      Instances For
        theorem ZMod.completedLFunction_eq {N : } [NeZero N] (Φ : ZMod N) (s : ) :
        ZMod.completedLFunction Φ s = ZMod.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) :

        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) :

        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) :

        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 : ) :
        ZMod.LFunction Φ s = ZMod.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) :
        ZMod.completedLFunction Φ (1 - s) = N ^ (s - 1) * ZMod.completedLFunction (ZMod.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 : ) :
        ZMod.completedLFunction Φ (1 - s) = N ^ (s - 1) * Complex.I * ZMod.completedLFunction (ZMod.dft Φ) s

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