English
For a normed complete ring-valued multiplicative function f with f(0)=0 and f(1)=1, the Euler product converges to the sum ∑ f(n): ∏' p ∑' e f(p^e) = ∑' n f(n).
Русский
Для нормированной полной кольцевой шкалы мультипликативной функции f с f(0)=0 и f(1)=1 Эйлерово произведение сходится к сумме ∑ f(n): ∏' p ∑' e f(p^e) = ∑' n f(n).
LaTeX
$$$\\text{HasProd}\\ (p\\mapsto \\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 terms of `HasProd`. -/
nonrec theorem eulerProduct_hasProd {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable (‖f ·‖)) :
HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n) :=
eulerProduct_hasProd hf.1 hf.2 hsum f.map_zero
