English
For DirichletCharacter χ modulo N and Re(s) > 1, Tendsto of partial products converges to L(χ, s): ∏_{p ≤ p_n} (1 − χ(p) p^{−s})^{−1} → L(χ, s).
Русский
Для Dirichlet-символа χ по модулю N и Re(s) > 1 частичные произведения сходятся к L(χ, s): ∏_{p ≤ p_n} (1 − χ(p) p^{−s})^{−1} → L(χ, s).
LaTeX
$$$\text{Tendsto}\Big(\!\lambda n. \prod_{p \le p_n}(1 - χ(p) p^{-s})^{-1}\Big)_{n\to\infty} = \text{nhds}(L(χ, s)).$$$
Lean4
/-- 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 LSeries_eulerProduct {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - χ p * (p : ℂ) ^ (-s))⁻¹) atTop (𝓝 (L (↗χ) s)) :=
by
rw [← tsum_dirichletSummand χ hs]
apply eulerProduct_completely_multiplicative <| summable_dirichletSummand χ hs
