English
The Euler product for completely multiplicative functions holds in the form ∏' p (1 - f(p))^{-1} = ∑' n f(n) under summability of ‖f‖.
Русский
Эйлерово произведение для полностью мультипликативной функции имеет вид ∏' p (1 - f(p))^{-1} = ∑' n f(n) при суммируемости по ‖f‖.
LaTeX
$$$\\prod_{p\\in Primes} (1 - f(p))^{-1} = \\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` is
multiplicative on coprime arguments, and `‖f ·‖` is summable, then
`∏' p : {p : ℕ | p.Prime}, ∑' e, f (p ^ e) = ∑' n, f n`.
This is a version using convergence of finite partial products. -/
theorem eulerProduct (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, ∑' e, f (p ^ e)) atTop (𝓝 (∑' n, f n)) :=
by
have := (eulerProduct_hasProd_mulIndicator hf₁ hmul hsum hf₀).tendsto_prod_nat
let F : ℕ → R := fun p ↦ ∑' (e : ℕ), f (p ^ e)
have H (n : ℕ) : ∏ i ∈ range n, Set.mulIndicator {p | Nat.Prime p} F i = ∏ p ∈ primesBelow n, ∑' (e : ℕ), f (p ^ e) :=
prod_mulIndicator_eq_prod_filter (range n) (fun _ ↦ F) (fun _ ↦ {p | Nat.Prime p}) id
simpa only [F, H]
