English
Let f be Summable with f(0)=0. Then for any N, the norm-summable property holds for N.smoothNumbers and the HasSum matches the finite prime product expression: sum over smooth numbers equals product over primes Below N of sums over p^n.
Русский
Пусть f суммируема, f(0)=0. Для любого N нормируемая сумма по N-склоняемым числам совпадает с произведением по простым ниже N.
LaTeX
$$$\\forall N:\\ Summable_{m\\in N.smoothNumbers} \\|f(m)\\| \\land HasSum_{m\\in N.smoothNumbers} f(m) = \\prod_{p\\in N.primesBelow} \\sum_{n\\ge0} f(p^n).$$$
Lean4
/-- A version of `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum`
in terms of the value of the series. -/
theorem prod_primesBelow_tsum_eq_tsum_smoothNumbers (hsum : Summable (‖f ·‖)) (N : ℕ) :
∏ p ∈ N.primesBelow, ∑' n : ℕ, f (p ^ n) = ∑' m : N.smoothNumbers, f m :=
(summable_and_hasSum_smoothNumbers_prod_primesBelow_tsum hf₁ hmul
(fun hp ↦ hsum.comp_injective <| Nat.pow_right_injective hp.one_lt) _).2.tsum_eq.symm
