English
Under hypotheses of norm-summability and coprime multiplicativity, the Euler product converges to the standard Dirichlet series sum: the product over primes of the local sums equals the global sum of f(n).
Русский
При предположениях суммируемости по нормам и мультипликативности на попарно взаимно простых аргументах, Эйлерово произведение сходится к сумме по всем n.
LaTeX
$$$\\sum_{n\\ge0} f(n) = \\prod_{p\\text{ prime}} \\sum_{e\\ge0} 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 : Nat.Primes, ∑' e, f (p ^ e) = ∑' n, f n`. This version is stated using `HasProd`. -/
theorem eulerProduct_hasProd (hsum : Summable (‖f ·‖)) (hf₀ : f 0 = 0) :
HasProd (fun p : Primes ↦ ∑' e, f (p ^ e)) (∑' n, f n) :=
by
let F : ℕ → R := fun n ↦ ∑' e, f (n ^ e)
change HasProd (F ∘ Subtype.val (p := (· ∈ {x | Nat.Prime x}))) _
rw [hasProd_subtype_iff_mulIndicator, HasProd, SummationFilter.unconditional, Metric.tendsto_atTop]
intro ε hε
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum.of_norm hf₀ hε
refine ⟨range N₀, fun s hs ↦ ?_⟩
have : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with p.Prime, F p :=
prod_mulIndicator_eq_prod_filter s (fun _ ↦ F) _ id
rw [this, dist_eq_norm, prod_filter_prime_tsum_eq_tsum_factoredNumbers hf₁ hmul hsum, norm_sub_rev]
exact hN₀ s fun p hp ↦ hs <| mem_range.mpr <| lt_of_mem_primesBelow hp
