English
For a completely multiplicative f : ℕ →*₀ F into a complete normed field F with ∑ ‖f‖ convergent, the Euler product holds: ∏' p : Primes, (1 − f(p))^{-1} = ∑' n f(n).
Русский
Для полностью мультипликативной f : ℕ →*₀ F в полном нормированном поле F и сходящейся суммы ∑ ‖f‖ выполняется Эйлерово произведение: ∏' p (1 − f(p))^{-1} = ∑' n f(n).
LaTeX
$$$\\prod_{p\\in Primes} (1 - f(p))^{-1} = \\sum_{n\\ge0} f(n).$$$
Lean4
/-- The *Euler Product* for completely multiplicative functions.
If `f : ℕ →*₀ F`, where `F` is a complete normed field and `‖f ·‖` is summable, then
`∏' p : Nat.Primes, (1 - f p)⁻¹ = ∑' n, f n`.
This version is stated in terms of `HasProd`. -/
theorem eulerProduct_completely_multiplicative_hasProd {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
HasProd (fun p : Primes ↦ (1 - f p)⁻¹) (∑' n, f n) :=
by
have H : (fun p : Primes ↦ (1 - f p)⁻¹) = fun p : Primes ↦ ∑' (e : ℕ), f (p ^ e) :=
funext <| fun p ↦ one_sub_inv_eq_geometric_of_summable_norm p.prop hsum
simpa only [map_pow, H] using eulerProduct_hasProd f.map_one (fun {m n} _ ↦ f.map_mul m n) hsum f.map_zero
