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

The first main result of this file is riemannZeta_eulerProduct, which states 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). The formalized statement is the second equality above, since infinite products are not yet available in Mathlib.

The second result is dirichletLSeries_eulerProduct, which is the analogous statement for Dirichlet L-functions.

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 = { toZeroHom := { 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 = { toZeroHom := { 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 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 riemannZeta_eulerProduct {s : ℂ} (hs : 1 < s.re) : Filter.Tendsto (fun (n : ℕ) => Finset.prod (Nat.primesBelow n) fun (p : ℕ) => (1 - ↑p ^ (-s))⁻¹) Filter.atTop (nhds (riemannZeta s))

The Euler product for the Riemann ζ function, valid for s.re > 1.

theorem dirichletLSeries_eulerProduct {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) : Filter.Tendsto (fun (n : ℕ) => Finset.prod (Nat.primesBelow n) fun (p : ℕ) => (1 - χ ↑p * ↑p ^ (-s))⁻¹) Filter.atTop (nhds (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n))

The Euler product for Dirichlet L-series, valid for s.re > 1.