prod_filter_prime_geometric_eq_tsum_factoredNumbers

English

Given a multiplicative f with ∑ ‖f‖ summable, the geometric product over primes in s equals the tsum over factoredNumbers(s): ∏ p∈s with p.Prime (1 − f(p))^{-1} = ∑' m : factoredNumbers s, f m.

Русский

При мультипликативной f со схождением ∑ ‖f‖ геометрическое произведение по простым в s равно tsum по factoredNumbers(s).

LaTeX

$$$\\prod_{p\\in s, p\\text{Prime}} (1 - f(p))^{-1} = \\sum_{m\\in \\mathrm{factoredNumbers}(s)} f(m).$$$

Lean4

/-- A version of `EulerProduct.summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric`
in terms of the value of the series. -/
theorem prod_filter_prime_geometric_eq_tsum_factoredNumbers {f : ℕ →* F} (hsum : Summable f) (s : Finset ℕ) :
    ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ = ∑' m : factoredNumbers s, f m :=
  by
  refine (summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric ?_ s).2.tsum_eq.symm
  exact fun {_} hp ↦ hsum.norm_lt_one hp.one_lt

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