English
A variant of the Euler product in terms of exponentials and sums of logarithms: exp(∑' p, −log(1 − f(p))) = ∑' n f(n) for f: primes → ℂ summable in norm.
Русский
Вариант Эйлерова произведения через экспоненту и сумму логарифмов: exp(∑' p, −log(1 − f(p))) = ∑' n f(n) для f : простые → ℂ с суммируемостью по норме.
LaTeX
$$$\forall f: \text{MonoidWithZeroHom}(\mathbb{N}, \mathbb{C}),\; \text{Summable } \|f\| \Rightarrow \exp\Big(\sum_{p \text{ prime}} -\log\bigl(1 - f(p)\bigr)\Big) = \sum_{n=1}^{\infty} f(n).$$$
Lean4
/-- A variant of the Euler Product formula in terms of the exponential of a sum of logarithms. -/
theorem exp_tsum_primes_log_eq_tsum {f : ℕ →*₀ ℂ} (hsum : Summable (‖f ·‖)) :
exp (∑' p : Nat.Primes, -log (1 - f p)) = ∑' n : ℕ, f n :=
by
have hs {p : ℕ} (hp : 1 < p) : ‖f p‖ < 1 := hsum.of_norm.norm_lt_one (f := f.toMonoidHom) hp
have hp (p : Nat.Primes) : 1 - f p ≠ 0 := fun h ↦ (norm_one (α := ℂ) ▸ (sub_eq_zero.mp h) ▸ hs p.prop.one_lt).false
have H := hsum.of_norm.clog_one_sub.neg.subtype {p | p.Prime} |>.hasSum.cexp.tprod_eq
simp only [Set.coe_setOf, Set.mem_setOf_eq, Function.comp_apply, exp_neg, exp_log (hp _)] at H
exact H.symm.trans <| eulerProduct_completely_multiplicative_tprod hsum
