prod_primesBelow_geometric_eq_tsum_smoothNumbers

English

For f with ∑ ‖f‖ summable and f(1)=1, the tsum over primesBelow with geometric weights equals the tsum over smoothNumbers.

Русский

Для f со суммируемостью норм и f(1)=1, tsum по primesBelow с геометрическими весами равен tsum по smoothNumbers.

LaTeX

$$$\\sum_{p\\in N.primesBelow} \\sum_{e\\ge0} f(p^e) = \\sum_{m\\in N.smoothNumbers} f(m).$$$

Lean4

/-- A version of `EulerProduct.summable_and_hasSum_smoothNumbers_prod_primesBelow_geometric`
in terms of the value of the series. -/
theorem prod_primesBelow_geometric_eq_tsum_smoothNumbers {f : ℕ →* F} (hsum : Summable f) (N : ℕ) :
    ∏ p ∈ N.primesBelow, (1 - f p)⁻¹ = ∑' m : N.smoothNumbers, f m :=
  by
  rw [smoothNumbers_eq_factoredNumbers, primesBelow]
  exact prod_filter_prime_geometric_eq_tsum_factoredNumbers hsum _

Похожие утверждения