English
The Euler product for completely multiplicative functions: for a completely multiplicative f: ℕ → F into a complete normed field F, with ∑ ‖f‖ convergent, we have ∏' p (1 − f(p))^{-1} = ∑' n f(n).
Русский
Эйлерово произведение для полностью мультипликативной функции: при f: ℕ → F в completo нормированном поле F и суммируемости по нормам выполняется ∏' p (1 − f(p))^{-1} = ∑' n f(n).
LaTeX
$$$\\text{HasProd}\\ Bigl(\\lambda p: Primes,\\ (1 - f(p))^{-1}\\Bigr) = \\sum_{n\\ge0} f(n).$$$
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` i
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : ℕ, if p.Prime then ∑' e, f (p ^ e) else 1 = ∑' n, f n`.
This version is stated using `HasProd` and `Set.mulIndicator`. -/
theorem eulerProduct_hasProd_mulIndicator (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
HasProd (Set.mulIndicator {p | Nat.Prime p} fun p ↦ ∑' e, f (p ^ e)) (∑' n, f n) :=
by
rw [← hasProd_subtype_iff_mulIndicator]
exact eulerProduct_hasProd hf₁ hmul hsum hf₀
