Documentation

Mathlib.NumberTheory.EulerProduct.DirichletLSeries

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.

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

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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem summable_riemannZetaSummand {s : ℂ} (hs : 1 < s.re) :
      Summable fun (n : ℕ) => ‖(riemannZetaSummandHom (_ : s ≠ 0)) n‖

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

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

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

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

      source
      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 χ (_ : s ≠ 0)) n))

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