English
If f is a completely multiplicative function from natural numbers to a normed field and ∑ ‖f(n)‖ converges, then for any prime p, the geometric series ∑_{e≥0} f(p^e) sums to (1 − f(p))^{-1}. The convergence is absolute.
Русский
Если f — полностью мультипликативная функция из натуральных чисел в нормированное поле, и ∑ ‖f(n)‖ сходится, то для любого простого p геометрическая серия ∑_{e≥0} f(p^e) сходится к (1 − f(p))^{-1}. Сходимость абсолютная.
LaTeX
$$$\\forall p\\text{ prime}:(1 - f(p))^{-1} = \\sum_{e=0}^{\\infty} f(p^e).$$$
Lean4
theorem one_sub_inv_eq_geometric_of_summable_norm {f : ℕ →*₀ F} {p : ℕ} (hp : p.Prime) (hsum : Summable fun x ↦ ‖f x‖) :
(1 - f p)⁻¹ = ∑' (e : ℕ), f (p ^ e) := by
simp only [map_pow]
refine (tsum_geometric_of_norm_lt_one <| summable_geometric_iff_norm_lt_one.mp ?_).symm
refine Summable.of_norm ?_
simpa only [Function.comp_def, map_pow] using hsum.comp_injective <| Nat.pow_right_injective hp.one_lt
