English
Let f be a multiplicative function with f(1)=1 and f(0)=0, taking values in a complete normed ring, and suppose ∑ ‖f‖ converges. Then the finite Euler product over primes in s equals the sum over factoredNumbers(s).
Русский
Пусть f — мультипликативная функция, f(1)=1, f(0)=0, значения в полуме normированном полной кольце, и пусть сумма норм сходится. Тогда конечный Эйлерово произведение по простым в s равно сумме по числам, разложенным по s.
LaTeX
$$$\\forall s:\\ Finset\\mathbb N:\\prod_{p\\in s,\\ p\\text{ Prime}} \\sum_{n\\ge0} f(p^n) = \\sum_{m\\in\\mathrm{factoredNumbers}(s)} f(m).$$$
Lean4
/-- A version of `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum`
in terms of the value of the series. -/
theorem prod_filter_prime_tsum_eq_tsum_factoredNumbers (hsum : Summable (‖f ·‖)) (s : Finset ℕ) :
∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n) = ∑' m : factoredNumbers s, f m :=
(summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum hf₁ hmul
(fun hp ↦ hsum.comp_injective <| Nat.pow_right_injective hp.one_lt) _).2.tsum_eq.symm
