English
If f is multiplicative and summable, then for any prime p, the geometric series ∑ f(p^e) converges to (1 − f(p))^{-1}. Moreover, the norm of f(p^e) decays geometrically, ensuring absolute convergence.
Русский
Если f — мультипликативная и суммируема, то геометрическая серия ∑ f(p^e) сходится к (1 − f(p))^{-1}, а нормы |f(p^e)| убывают геометрически, обеспечивая абсолютную сходимость.
LaTeX
$$$\\forall p\\text{ prime}: (1 - f(p))^{-1} = \\sum_{e=0}^{\\infty} f(p^{e}).$$$
Lean4
/-- The *Euler Product* for multiplicative (on coprime arguments) functions.
If `f : ℕ → R`, where `R` is a complete normed commutative ring, `f 0 = 0`, `f 1 = 1`, `f` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n`. -/
theorem eulerProduct_tprod (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) : ∏' p : Primes, ∑' e, f (p ^ e) = ∑' n, f n :=
(eulerProduct_hasProd hf₁ hmul hsum hf₀).tprod_eq
