Documentation

Mathlib.NumberTheory.LSeries.Dirichlet

L-series of Dirichlet characters and arithmetic functions #

We collect some results on L-series of specific (arithmetic) functions, for example, the Möbius function μ or the von Mangoldt function Λ. In particular, we show that L ↗Λ is the negative of the logarithmic derivative of the Riemann zeta function on re s > 1; see LSeries_vonMangoldt_eq_deriv_riemannZeta_div.

We also prove some general results on L-series associated to Dirichlet characters (i.e., Dirichlet L-series). For example, we show that the abscissa of absolute convergence equals 1 (see DirichletCharacter.absicssaOfAbsConv) and that the L-series does not vanish on the open half-plane re s > 1 (see DirichletCharacter.LSeries_ne_zero_of_one_lt_re).

We deduce results on the Riemann zeta function (which is L 1 or L ↗ζ on re s > 1) as special cases.

Tags #

Dirichlet L-series, Möbius function, von Mangoldt function, Riemann zeta function

δ is the function underlying the arithmetic function 1.

The L-series of the Möbius function #

We show that L μ s converges absolutely if and only if re s > 1.

theorem ArithmeticFunction.not_LSeriesSummable_moebius_at_one :
¬LSeriesSummable (fun (n : ) => (ArithmeticFunction.moebius n)) 1
theorem ArithmeticFunction.LSeriesSummable_moebius_iff {s : } :
LSeriesSummable (fun (n : ) => (ArithmeticFunction.moebius n)) s 1 < s.re

The L-series of the Möbius function converges absolutely at s if and only if re s > 1.

theorem ArithmeticFunction.abscissaOfAbsConv_moebius :
(LSeries.abscissaOfAbsConv fun (n : ) => (ArithmeticFunction.moebius n)) = 1

The abscissa of absolute convergence of the L-series of the Möbius function is 1.

L-series of Dirichlet characters #

theorem ArithmeticFunction.const_one_eq_zeta {R : Type u_1} [Semiring R] {n : } (hn : n 0) :
1 n = ((fun (x : ) => ArithmeticFunction.zeta x) n)
theorem LSeries.one_convolution_eq_zeta_convolution {R : Type u_1} [Semiring R] (f : R) :
LSeries.convolution 1 f = LSeries.convolution (fun (x : ) => (ArithmeticFunction.zeta x)) f
theorem LSeries.convolution_one_eq_convolution_zeta {R : Type u_1} [Semiring R] (f : R) :
LSeries.convolution f 1 = LSeries.convolution f fun (x : ) => (ArithmeticFunction.zeta x)

χ₁ is (local) notation for the (necessarily trivial) Dirichlet character modulo 1.

Equations
Instances For
    theorem DirichletCharacter.mul_convolution_distrib {R : Type u_1} [CommSemiring R] {n : } (χ : DirichletCharacter R n) (f : R) (g : R) :
    LSeries.convolution ((fun (x : ) => χ x) * f) ((fun (x : ) => χ x) * g) = (fun (x : ) => χ x) * LSeries.convolution f g

    Twisting by a Dirichlet character χ distributes over convolution.

    theorem DirichletCharacter.convolution_mul_moebius {n : } (χ : DirichletCharacter n) :
    LSeries.convolution (fun (n_1 : ) => χ n_1) ((fun (n_1 : ) => χ n_1) * fun (n : ) => (ArithmeticFunction.moebius n)) = LSeries.delta

    The convolution of a Dirichlet character χ with the twist χ * μ is δ, the indicator function of {1}.

    The Dirichlet character mod 0 corresponds to δ.

    theorem DirichletCharacter.modOne_eq_one {R : Type u_1} [CommSemiring R] {χ : DirichletCharacter R 1} :
    (fun (x : ) => χ x) = 1

    The Dirichlet character mod 1 corresponds to the constant function 1.

    theorem DirichletCharacter.not_LSeriesSummable_at_one {N : } (hN : N 0) (χ : DirichletCharacter N) :
    ¬LSeriesSummable (fun (n : ) => χ n) 1

    The L-series of a Dirichlet character mod N > 0 does not converge absolutely at s = 1.

    theorem DirichletCharacter.LSeriesSummable_of_one_lt_re {N : } (χ : DirichletCharacter N) {s : } (hs : 1 < s.re) :
    LSeriesSummable (fun (n : ) => χ n) s

    The L-series of a Dirichlet character converges absolutely at s if re s > 1.

    theorem DirichletCharacter.LSeriesSummable_iff {N : } (hN : N 0) (χ : DirichletCharacter N) {s : } :
    LSeriesSummable (fun (n : ) => χ n) s 1 < s.re

    The L-series of a Dirichlet character mod N > 0 converges absolutely at s if and only if re s > 1.

    theorem DirichletCharacter.absicssaOfAbsConv_eq_one {N : } (hn : N 0) (χ : DirichletCharacter N) :
    (LSeries.abscissaOfAbsConv fun (n : ) => χ n) = 1

    The abscissa of absolute convergence of the L-series of a Dirichlet character mod N > 0 is 1.

    theorem DirichletCharacter.LSeriesSummable_mul {N : } (χ : DirichletCharacter N) {f : } {s : } (h : LSeriesSummable f s) :
    LSeriesSummable ((fun (n : ) => χ n) * f) s

    The L-series of the twist of f by a Dirichlet character converges at s if the L-series of f does.

    theorem DirichletCharacter.LSeries.mul_mu_eq_one {N : } (χ : DirichletCharacter N) {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => χ n) s * LSeries ((fun (n : ) => χ n) * fun (n : ) => (ArithmeticFunction.moebius n)) s = 1

    The L-series of a Dirichlet character χ and of the twist of μ by χ are multiplicative inverses.

    L-series of Dirichlet characters do not vanish on re s > 1 #

    theorem DirichletCharacter.LSeries_ne_zero_of_one_lt_re {N : } (χ : DirichletCharacter N) {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => χ n) s 0

    The L-series of a Dirichlet character does not vanish on the right half-plane re s > 1.

    The L-series of the constant sequence 1 / the arithmetic function ζ #

    Both give the same L-series (since the difference in values at zero has no effect; see ArithmeticFunction.LSeries_zeta_eq), which agrees with the Riemann zeta function on re s > 1. We state most results in two versions, one for 1 and one for ↗ζ.

    The abscissa of (absolute) convergence of the constant sequence 1 is 1.

    theorem LSeriesSummable_one_iff {s : } :
    LSeriesSummable 1 s 1 < s.re

    The LSeries of the constant sequence 1 converges at s if and only if re s > 1.

    theorem ArithmeticFunction.LSeries_zeta_eq :
    (LSeries fun (n : ) => (ArithmeticFunction.zeta n)) = LSeries 1

    The LSeries of the arithmetic function ζ is the same as the LSeries associated to the constant sequence 1.

    theorem ArithmeticFunction.LSeriesSummable_zeta_iff {s : } :
    LSeriesSummable (fun (x : ) => (ArithmeticFunction.zeta x)) s 1 < s.re

    The LSeries associated to the arithmetic function ζ converges at s if and only if re s > 1.

    @[deprecated ArithmeticFunction.LSeriesSummable_zeta_iff]
    theorem ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re {s : } :
    LSeriesSummable (fun (x : ) => (ArithmeticFunction.zeta x)) s 1 < s.re

    Alias of ArithmeticFunction.LSeriesSummable_zeta_iff.


    The LSeries associated to the arithmetic function ζ converges at s if and only if re s > 1.

    theorem ArithmeticFunction.abscissaOfAbsConv_zeta :
    (LSeries.abscissaOfAbsConv fun (n : ) => (ArithmeticFunction.zeta n)) = 1

    The abscissa of (absolute) convergence of the arithmetic function ζ is 1.

    theorem ArithmeticFunction.LSeries_zeta_eq_riemannZeta {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => (ArithmeticFunction.zeta n)) s = riemannZeta s

    The L-series of the arithmetic function ζ equals the Riemann Zeta Function on its domain of convergence 1 < re s.

    theorem ArithmeticFunction.LSeriesHasSum_zeta {s : } (hs : 1 < s.re) :
    LSeriesHasSum (fun (n : ) => (ArithmeticFunction.zeta n)) s (riemannZeta s)

    The L-series of the arithmetic function ζ equals the Riemann Zeta Function on its domain of convergence 1 < re s.

    theorem ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => (ArithmeticFunction.zeta n)) s * LSeries (fun (n : ) => (ArithmeticFunction.moebius n)) s = 1

    The L-series of the arithmetic function ζ and of the Möbius function are inverses.

    theorem ArithmeticFunction.LSeries_zeta_ne_zero_of_one_lt_re {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => (ArithmeticFunction.zeta n)) s 0

    The L-series of the arithmetic function ζ does not vanish on the right half-plane re s > 1.

    theorem LSeries_one_eq_riemannZeta {s : } (hs : 1 < s.re) :

    The L-series of the constant sequence 1 equals the Riemann Zeta Function on its domain of convergence 1 < re s.

    theorem LSeriesHasSum_one {s : } (hs : 1 < s.re) :

    The L-series of the constant sequence 1 equals the Riemann zeta function on its domain of convergence 1 < re s.

    theorem LSeries_one_mul_Lseries_moebius {s : } (hs : 1 < s.re) :
    LSeries 1 s * LSeries (fun (n : ) => (ArithmeticFunction.moebius n)) s = 1

    The L-series of the constant sequence 1 and of the Möbius function are inverses.

    theorem LSeries_one_ne_zero_of_one_lt_re {s : } (hs : 1 < s.re) :
    LSeries 1 s 0

    The L-series of the constant sequence 1 does not vanish on the right half-plane re s > 1.

    theorem riemannZeta_ne_zero_of_one_lt_re {s : } (hs : 1 < s.re) :

    The Riemann Zeta Function does not vanish on the half-plane re s > 1.

    The L-series of the von Mangoldt function #

    theorem ArithmeticFunction.convolution_vonMangoldt_zeta :
    (LSeries.convolution (fun (n : ) => (ArithmeticFunction.vonMangoldt n)) fun (n : ) => (ArithmeticFunction.zeta n)) = fun (n : ) => Complex.log n

    A translation of the relation Λ * ↑ζ = log of (real-valued) arithmetic functions to an equality of complex sequences.

    theorem ArithmeticFunction.convolution_vonMangoldt_const_one :
    LSeries.convolution (fun (n : ) => (ArithmeticFunction.vonMangoldt n)) 1 = fun (n : ) => Complex.log n
    theorem ArithmeticFunction.LSeriesSummable_vonMangoldt {s : } (hs : 1 < s.re) :
    LSeriesSummable (fun (n : ) => (ArithmeticFunction.vonMangoldt n)) s

    The L-series of the von Mangoldt function Λ converges at s when re s > 1.

    theorem DirichletCharacter.convolution_twist_vonMangoldt {N : } (χ : DirichletCharacter N) :
    (LSeries.convolution ((fun (n : ) => χ n) * fun (n : ) => (ArithmeticFunction.vonMangoldt n)) fun (n : ) => χ n) = (fun (n : ) => χ n) * fun (n : ) => Complex.log n

    A twisted version of the relation Λ * ↑ζ = log in terms of complex sequences.

    theorem DirichletCharacter.LSeriesSummable_twist_vonMangoldt {N : } (χ : DirichletCharacter N) {s : } (hs : 1 < s.re) :
    LSeriesSummable ((fun (n : ) => χ n) * fun (n : ) => (ArithmeticFunction.vonMangoldt n)) s

    The L-series of the twist of the von Mangoldt function Λ by a Dirichlet character χ converges at s when re s > 1.

    theorem DirichletCharacter.LSeries_twist_vonMangoldt_eq {N : } (χ : DirichletCharacter N) {s : } (hs : 1 < s.re) :
    LSeries ((fun (n : ) => χ n) * fun (n : ) => (ArithmeticFunction.vonMangoldt n)) s = -deriv (LSeries fun (n : ) => χ n) s / LSeries (fun (n : ) => χ n) s

    The L-series of the twist of the von Mangoldt function Λ by a Dirichlet character χ at s equals the negative logarithmic derivative of the L-series of χ when re s > 1.

    theorem ArithmeticFunction.LSeries_vonMangoldt_eq {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => (ArithmeticFunction.vonMangoldt n)) s = -deriv (LSeries 1) s / LSeries 1 s

    The L-series of the von Mangoldt function Λ equals the negative logarithmic derivative of the L-series of the constant sequence 1 on its domain of convergence re s > 1.

    theorem ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div {s : } (hs : 1 < s.re) :
    LSeries (fun (n : ) => (ArithmeticFunction.vonMangoldt n)) s = -deriv riemannZeta s / riemannZeta s

    The L-series of the von Mangoldt function Λ equals the negative logarithmic derivative of the Riemann zeta function on its domain of convergence re s > 1.