English
If a function f is Multipliable and supported only on prime powers, then the total product over all n factors into a product over primes p and powers k+1, i.e., a prime-power factorization of the Dirichlet-type product.
Русский
Если f меромерна ( Multipliable ) и поддержка сосредоточена только на простых степенях, то произведение по всем n раскладывается на произведение по простым p и степеням k+1, т. е. разложение по простым степеням.
LaTeX
$$$\prod_{n} f(n) = \prod_{p \in \text{Primes}} \prod_{k\ge 0} f(p^{k+1})$$$
Lean4
@[to_additive tsum_eq_tsum_primes_of_support_subset_prime_powers]
theorem tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers {f : ℕ → α} (hfm : Multipliable f)
(hf : Function.mulSupport f ⊆ {n | IsPrimePow n}) : ∏' n : ℕ, f n = ∏' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 1)) :=
by
have hfm' : Multipliable fun pk : Nat.Primes × ℕ ↦ f (pk.fst ^ (pk.snd + 1)) :=
prodNatEquiv.symm.multipliable_iff.mp <| by
simpa only [← coe_prodNatEquiv_apply, Prod.eta, Function.comp_def, Equiv.apply_symm_apply] using hfm.subtype _
simp only [← tprod_subtype_eq_of_mulSupport_subset hf, Set.coe_setOf, ← prodNatEquiv.tprod_eq, ← hfm'.tprod_prod]
refine tprod_congr fun (p, k) ↦ congrArg f <| coe_prodNatEquiv_apply ..
