LSeries_eulerProduct_hasProd — Mathlib

English

For DirichletCharacter χ modulo N and Re(s) > 1, HasProd over primes of (1 − χ(p) p^{−s})^{−1} equals L(χ, s).

Русский

Для Дирихлетового символа χ по модулю N и Re(s) > 1 имеет место HasProd по простым p: (1 − χ(p) p^{−s})^{−1} = L(χ, s).

LaTeX

$$$\text{HasProd}\Big(p \mapsto \bigl(1 - χ(p) p^{-s}\bigr)^{-1}, L(χ, s)\Big)\;\text{при } \Re(s) > 1.$$$

Lean4

/-- The Euler product for Dirichlet L-series, valid for `s.re > 1`.
This version is stated in terms of `HasProd`. -/
theorem LSeries_eulerProduct_hasProd {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
    HasProd (fun p : Primes ↦ (1 - χ p * (p : ℂ) ^ (-s))⁻¹) (L (↗χ) s) :=
  by
  rw [← tsum_dirichletSummand χ hs]
  convert eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

Похожие утверждения