English
For a multiplicative f with ∑ ‖f(n)‖ summable, and p prime, the sum over e of f(p^e) is absolutely summable and equals the geometric expression (1 − f(p))^{-1}. This extends to finite subsets s of primes with appropriate normalization.
Русский
При мультипликативности f и суммируемости ∑ ‖f(n)‖ сумма по e для каждого простого p сходится absolutely и равна (1 − f(p))^{-1}; распространяется на конечные подмножества простых.
LaTeX
$$$\\forall p\\Prm{prime}:\\sum_{e\\ge0} f(p^e) = (1 - f(p))^{-1}.$$$
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 `s`-factored
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p ∈ s`. At the same time,
we show that the sum involved converges absolutely. -/
theorem summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric {f : ℕ →* F}
(h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) (s : Finset ℕ) :
Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
HasSum (fun m : factoredNumbers s ↦ f m) (∏ p ∈ s with p.Prime, (1 - f p)⁻¹) :=
by
have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
have H₁ : ∏ p ∈ s with p.Prime, ∑' n : ℕ, f (p ^ n) = ∏ p ∈ s with p.Prime, (1 - f p)⁻¹ :=
by
refine prod_congr rfl fun p hp ↦ ?_
simp only [map_pow]
exact tsum_geometric_of_norm_lt_one <| h (mem_filter.mp hp).2
have H₂ : ∀ {p : ℕ}, p.Prime → Summable fun n ↦ ‖f (p ^ n)‖ :=
by
intro p hp
simp only [map_pow]
refine Summable.of_nonneg_of_le (fun _ ↦ norm_nonneg _) (fun _ ↦ norm_pow_le ..) ?_
exact summable_geometric_iff_norm_lt_one.mpr <| (norm_norm (f p)).symm ▸ h hp
exact H₁ ▸ summable_and_hasSum_factoredNumbers_prod_filter_prime_tsum f.map_one hmul H₂ s
