Logarithms of Euler Products

Here we consider f : ℕ →*₀ ℂ and the goal is to prove that exp (∑ p in Primes, log (1 - f p)⁻¹) = ∑ n : ℕ, f n under suitable conditions on f.

theorem sum_primesBelow_eq_sum_range_indicator {R : Type u_1} [AddCommMonoid R] (f : ℕ → R) (n : ℕ) : ∑ p ∈ n.primesBelow, f p = ∑ m ∈ Finset.range n, {p : ℕ | Nat.Prime p}.indicator f m

theorem tendsto_sum_primesBelow_tsum {R : Type u_1} [AddCommGroup R] [UniformSpace R] [UniformAddGroup R] [CompleteSpace R] [T2Space R] {f : ℕ → R} (hsum : Summable f) : Filter.Tendsto (fun (n : ℕ) => ∑ p ∈ n.primesBelow, f p) Filter.atTop (nhds (∑' (p : Nat.Primes), f ↑p))

If f : ℕ → R is summable, then the limit as n tends to infinity of the sum of f p over the primes p < n is the same as the sum of f p over all primes.

theorem Complex.exp_tsum_primes {f : ℕ → ℂ} (hsum : Summable f) : Filter.Tendsto (fun (n : ℕ) => ∏ p ∈ n.primesBelow, Complex.exp (f p)) Filter.atTop (nhds (Complex.exp (∑' (p : Nat.Primes), f ↑p)))

If f : ℕ → ℂ is summable, then the limit as n tends to infinity of the product of exp (f p) over the primes p < n is the same as the exponential of the sum of f p over all primes.

theorem Summable.neg_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_sum_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.

theorem EulerProduct.exp_sum_primes_log_eq_tsum' {f : ℕ → ℂ} (h₀ : f 0 = 0) (h₁ : f 1 = 1) (hf : ∀ (m n : ℕ), f (m * n) = f m * f n) (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.