Documentation

Mathlib.NumberTheory.EulerProduct.ExpLog

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).

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