LSeries_zeta_eulerProduct_exp_log

English

A variant of the Euler product for the zeta function: exp(∑' p: Nat.Primes, −log(1 − p^{−s})) = L(1, s) = ζ(s).

Русский

Вариант Эйлерова произведения ζ-функции: exp(∑' p, −log(1 − p^{−s})) = L(1, s) = ζ(s).

LaTeX

$$$\forall s,\; \exp\Big(\sum_{p \text{ prime}} -\log(1 - p^{-s})\Big) = \zeta(s).$$$

Lean4

/-- A variant of the Euler product for the L-series of `ζ`. -/
theorem LSeries_zeta_eulerProduct_exp_log {s : ℂ} (hs : 1 < s.re) :
    exp (∑' p : Nat.Primes, -Complex.log (1 - p ^ (-s))) = L 1 s :=
  by
  convert modOne_eq_one (R := ℂ) ▸ DirichletCharacter.LSeries_eulerProduct_exp_log (1 : DirichletCharacter ℂ 1) hs using
    7
  rw [MulChar.one_apply <| isUnit_of_subsingleton _, one_mul]

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