Theorems · Theorem · number theory

EulerProduct.eulerProduct_completely_multiplicative

∀ {F : Type u_1} [inst : NormedField F] [CompleteSpace F] {f : ℕ →*₀ F},
  (Summable fun x => ‖f x‖) →
    Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - f p)⁻¹) Filter.atTop (nhds (∑' (n : ℕ), f n))

The Euler Product for completely multiplicative functions. If f : ℕ →*₀ F, where F is a complete normed field and ‖f ·‖ is summable, then ∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n. This version is stated in the form of convergence of finite partial products.

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

2 results in Mathlib

Foundations

Depth 173 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedFieldCompleteSpace