Logarithms of Euler Products

We consider f : ℕ →*₀ ℂ and show that exp (∑ p in Primes, log (1 - f p)⁻¹) = ∑ n : ℕ, f n under suitable conditions on f. This can be seen as a logarithmic version of the Euler product for f.

theorem Summable.clog_one_sub {α : Type u_1} {f : α → ℂ} (hsum : Summable f) : Summable fun (n : α) => Complex.log (1 - f n)

If f : α → ℂ is summable, then so is n ↦ log (1 - f n).

theorem EulerProduct.exp_tsum_primes_log_eq_tsum {f : ℕ →*₀ ℂ} (hsum : Summable fun (x : ℕ) => ‖f x‖) : Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - f ↑p)) = ∑' (n : ℕ), f n

A variant of the Euler Product formula in terms of the exponential of a sum of logarithms.