English
If f is a multiplicative function taking values in a complete normed ring, then the total product over primes of the local sums equals the total Dirichlet sum: ∏' p ∑' e f(p^e) = ∑' n f(n).
Русский
Если f — мультипликативная функция в полном нормированном кольце, то произведение по всем простым локальным суммам равно сумме по всем n: ∏' p ∑' e f(p^e) = ∑' n f(n).
LaTeX
$$$\\prod_{p\\in Primes} \\sum_{e\\ge0} f(p^e) = \\sum_{n\\ge0} f(n).$$$
Lean4
/-- 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. -/
nonrec theorem eulerProduct {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable (‖f ·‖)) :
Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, ∑' e, f (p ^ e)) atTop (𝓝 (∑' n, f n)) :=
eulerProduct hf.1 hf.2 hsum f.map_zero
