English
If f is multiplicative with |f(p)|<1 for all primes p, the product over primesBelow N of (1 − f(p))^{-1} equals tsum over N.smoothNumbers of f(m).
Русский
Если для всех простых p выполняется |f(p)|<1, то произведение по простым ниже N даёт эквивалентную сумму по N.smoothNumbers.
LaTeX
$$$\\prod_{p\\in N.primesBelow} (1 - f(p))^{-1} = \\sum_{m\\in N.smoothNumbers} f(m).$$$
Lean4
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `N`-smooth
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p < N`. At the same time,
we show that the sum involved converges absolutely. -/
theorem summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric {f : ℕ →* F} (h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1)
(N : ℕ) :
Summable (fun m : N.smoothNumbers ↦ ‖f m‖) ∧
HasSum (fun m : N.smoothNumbers ↦ f m) (∏ p ∈ N.primesBelow, (1 - f p)⁻¹) :=
by
rw [smoothNumbers_eq_factoredNumbers, primesBelow]
exact summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric h _
