English
A variant expressing L-series as the exponential of a log-sum: exp(∑' p (−log(1 − χ(p) p^{−s}))) = L(χ, s).
Русский
Вариант выражения L-функции через экспоненту от суммы логарифмов: exp(∑' p (−log(1 − χ(p) p^{−s}))) = L(χ, s).
LaTeX
$$$\forall s,\; \exp\Big(\sum_{p \text{ prime}} -\log\bigl(1 - χ(p) p^{-s}\bigr)\Big) = L(χ, s).$$$
Lean4
/-- A variant of the Euler product for Dirichlet L-series. -/
theorem LSeries_eulerProduct_exp_log {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ} (hs : 1 < s.re) :
exp (∑' p : Nat.Primes, -log (1 - χ p * p ^ (-s))) = L (↗χ) s :=
by
let f := dirichletSummandHom χ <| ne_zero_of_one_lt_re hs
have h n : term (↗χ) s n = f n := by
rcases eq_or_ne n 0 with rfl | hn
· simp only [term_zero, map_zero]
·
simp only [ne_eq, hn, not_false_eq_true, term_of_ne_zero, div_eq_mul_inv, dirichletSummandHom, cpow_neg,
MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, f]
simpa only [LSeries, h] using exp_tsum_primes_log_eq_tsum (f := f) <| summable_dirichletSummand χ hs
