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

theorem ArithmeticFunction.one_eq_delta : (fun (n : ℕ) => 1 n) = LSeries.delta

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

def Dchar_one : Lean.ParserDescr

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

Equations

• Dchar_one = Lean.ParserDescr.node `Dchar_one 1024 (Lean.ParserDescr.symbol "χ₁")

theorem DirichletCharacter.isMultiplicative_toArithmeticFunction {N : ℕ} {R : Type u_1} [CommMonoidWithZero R] (χ : DirichletCharacter R N) : (toArithmeticFunction fun (x : ℕ) => χ ↑x).IsMultiplicative

The arithmetic function associated to a Dirichlet character is multiplicative.

theorem DirichletCharacter.apply_eq_toArithmeticFunction_apply {N : ℕ} {R : Type u_1} [CommMonoidWithZero R] (χ : DirichletCharacter R N) {n : ℕ} (hn : n ≠ 0) : χ ↑n = (toArithmeticFunction fun (x : ℕ) => χ ↑x) n

theorem DirichletCharacter.mul_convolution_distrib {R : Type u_1} [CommSemiring R] {n : ℕ} (χ : DirichletCharacter R n) (f 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.mul_delta {n : ℕ} (χ : DirichletCharacter ℂ n) : (fun (n_1 : ℕ) => χ ↑n_1) * LSeries.delta = LSeries.delta

theorem DirichletCharacter.delta_mul {n : ℕ} (χ : DirichletCharacter ℂ n) : (LSeries.delta * fun (n_1 : ℕ) => χ ↑n_1) = LSeries.delta

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

theorem DirichletCharacter.modZero_eq_delta {χ : DirichletCharacter ℂ 0} : (fun (n : ℕ) => χ ↑n) = LSeries.delta

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.LSeries_modOne_eq : (LSeries fun (n : ℕ) => 1 ↑n) = LSeries 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 ↗ζ.

theorem LSeries.abscissaOfAbsConv_one : LSeries.abscissaOfAbsConv 1 = 1

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) : LSeries 1 s = riemannZeta s

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) : LSeriesHasSum 1 s (riemannZeta s)

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) : riemannZeta s ≠ 0

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.