English
Let F be a complete normed field. If f: N → F is completely multiplicative and ∑ ‖f‖ < ∞, then the finite prime products converge to the Dirichlet series: lim_{X→∞} ∏_{p ≤ X} (1 − f(p))^{-1} = ∑_{n≥1} f(n).
Русский
Пусть F — полное нормированное поле. Если f: N → F полностью мультипликативна и ∑ ‖f(n)‖ < ∞, то частичные Эйлеровы произведения сходятся к сумме ряда: lim_{X→∞} ∏_{p ≤ X} (1 − f(p))^{-1} = ∑_{n≥1} f(n).
LaTeX
$$$\forall f: \mathbb{N} \to F,\; (f(1)=1 \wedge \forall m,n, f(mn)=f(m)f(n) \wedge \sum_{n=1}^{\infty} \|f(n)\| < \infty) \Rightarrow \sum_{n=1}^{\infty} f(n) = \lim_{X \to \infty} \prod_{p \le X} (1 - f(p))^{-1}.$$$
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 the form of convergence of finite partial products. -/
theorem eulerProduct_completely_multiplicative {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - f p)⁻¹) atTop (𝓝 (∑' n, f n)) :=
by
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
have H (n : ℕ) :
∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p = ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
prod_mulIndicator_eq_prod_filter (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
have H' :
{p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
{p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
simpa only [← H, H'] using this
