The Euler Product for the Riemann Zeta Function and Dirichlet L-Series

The first main result of this file is the Euler Product formula for the Riemann ζ function $$\prod_p \frac{1}{1 - p^{-s}} = \lim_{n \to \infty} \prod_{p < n} \frac{1}{1 - p^{-s}} = \zeta(s)$$ for $s$ with real part $> 1$ ($p$ runs through the primes). riemannZeta_eulerProduct is the second equality above. There are versions riemannZeta_eulerProduct_hasProd and riemannZeta_eulerProduct_tprod in terms of HasProd and tprod, respectively.

The second result is dirichletLSeries_eulerProduct (with variants dirichletLSeries_eulerProduct_hasProd and dirichletLSeries_eulerProduct_tprod), which is the analogous statement for Dirichlet L-series.

noncomputable def riemannZetaSummandHom {s : ℂ} (hs : s ≠ 0) : ℕ →*₀ ℂ

When s ≠ 0, the map n ↦ n^(-s) is completely multiplicative and vanishes at zero.

Equations

• riemannZetaSummandHom hs = { toFun := fun (n : ℕ) => ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def dirichletSummandHom {s : ℂ} {n : ℕ} (χ : DirichletCharacter ℂ n) (hs : s ≠ 0) : ℕ →*₀ ℂ

When χ is a Dirichlet character and s ≠ 0, the map n ↦ χ n * n^(-s) is completely multiplicative and vanishes at zero.

Equations

• dirichletSummandHom χ hs = { toFun := fun (n_1 : ℕ) => χ ↑n_1 * ↑n_1 ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }

theorem summable_riemannZetaSummand {s : ℂ} (hs : 1 < s.re) : Summable fun (n : ℕ) => ‖(riemannZetaSummandHom ⋯) n‖

When s.re > 1, the map n ↦ n^(-s) is norm-summable.

theorem tsum_riemannZetaSummand {s : ℂ} (hs : 1 < s.re) : ∑' (n : ℕ), (riemannZetaSummandHom ⋯) n = riemannZeta s

theorem summable_dirichletSummand {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Summable fun (n : ℕ) => ‖(dirichletSummandHom χ ⋯) n‖

When s.re > 1, the map n ↦ χ(n) * n^(-s) is norm-summable.

theorem tsum_dirichletSummand {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : ∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = LSeries (fun (n : ℕ) => χ ↑n) s

theorem riemannZeta_eulerProduct_hasProd {s : ℂ} (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => (1 - ↑↑p ^ (-s))⁻¹) (riemannZeta s)

The Euler product for the Riemann ζ function, valid for s.re > 1. This version is stated in terms of HasProd.

theorem riemannZeta_eulerProduct_tprod {s : ℂ} (hs : 1 < s.re) : ∏' (p : Nat.Primes), (1 - ↑↑p ^ (-s))⁻¹ = riemannZeta s

The Euler product for the Riemann ζ function, valid for s.re > 1. This version is stated in terms of tprod.

theorem riemannZeta_eulerProduct {s : ℂ} (hs : 1 < s.re) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) Filter.atTop (nhds (riemannZeta s))

The Euler product for the Riemann ζ function, valid for s.re > 1. This version is stated in the form of convergence of finite partial products.

theorem DirichletCharacter.LSeries_eulerProduct_hasProd {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (LSeries (fun (n : ℕ) => χ ↑n) s)

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in terms of HasProd.

@[deprecated DirichletCharacter.LSeries_eulerProduct_hasProd]

theorem dirichletLSeries_eulerProduct_hasProd {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : HasProd (fun (p : Nat.Primes) => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (LSeries (fun (n : ℕ) => χ ↑n) s)

Alias of DirichletCharacter.LSeries_eulerProduct_hasProd.

---

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in terms of HasProd.

theorem DirichletCharacter.LSeries_eulerProduct_tprod {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : ∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = LSeries (fun (n : ℕ) => χ ↑n) s

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in terms of tprod.

@[deprecated DirichletCharacter.LSeries_eulerProduct_tprod]

theorem dirichlet_LSeries_eulerProduct_tprod {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : ∏' (p : Nat.Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹ = LSeries (fun (n : ℕ) => χ ↑n) s

Alias of DirichletCharacter.LSeries_eulerProduct_tprod.

---

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in terms of tprod.

theorem DirichletCharacter.LSeries_eulerProduct {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => χ ↑n) s))

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in the form of convergence of finite partial products.

@[deprecated DirichletCharacter.LSeries_eulerProduct]

theorem dirichletLSeries_eulerProduct {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (LSeries (fun (n : ℕ) => χ ↑n) s))

Alias of DirichletCharacter.LSeries_eulerProduct.

---

The Euler product for Dirichlet L-series, valid for s.re > 1. This version is stated in the form of convergence of finite partial products.

theorem DirichletCharacter.LSeries_eulerProduct_exp_log {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun (n : ℕ) => χ ↑n) s

A variant of the Euler product for Dirichlet L-series.

theorem ArithmeticFunction.LSeries_zeta_eulerProduct_exp_log {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = LSeries 1 s

A variant of the Euler product for the L-series of ζ.

theorem riemannZeta_eulerProduct_exp_log {s : ℂ} (hs : 1 < s.re) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - ↑↑p ^ (-s))) = riemannZeta s

A variant of the Euler product for the Riemann zeta function.

Changing the level of a Dirichlet L-series

theorem DirichletCharacter.LSeries_changeLevel {M N : ℕ} [NeZero N] (hMN : M ∣ N) (χ : DirichletCharacter ℂ M) {s : ℂ} (hs : 1 < s.re) : LSeries (fun (n : ℕ) => ((DirichletCharacter.changeLevel hMN) χ) ↑n) s = LSeries (fun (n : ℕ) => χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

If χ is a Dirichlet character and its level M divides N, then we obtain the L-series of χ considered as a Dirichlet character of level N from the L-series of χ by multiplying with ∏ p ∈ N.primeFactors, (1 - χ p * p ^ (-s)).