Theorems · Theorem · number theory

ArithmeticFunction.IsMultiplicative.eulerProduct

∀ {R : Type u_1} [inst : NormedCommRing R] [CompleteSpace R] {f : ArithmeticFunction R},
  f.IsMultiplicative →
    (Summable fun x => ‖f x‖) →
      Filter.Tendsto (fun n => ∏ p ∈ n.primesBelow, ∑' (e : ℕ), f (p ^ e)) Filter.atTop (nhds (∑' (n : ℕ), f n))

The Euler Product for a multiplicative arithmetic function f with values in a complete normed commutative ring R: if ‖f ·‖ is summable, then ∏' p : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n. This version is stated in the form of convergence of finite partial products.

Defined in

Mathlib.NumberTheory.EulerProduct.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedCommRingCompleteSpace