English
Under a multiplicability hypothesis and prime-power support, the total product equals a product over primes of the base values and a nested product over higher powers, giving a structured prime-factor decomposition.
Русский
При условии умножаемости и поддержки на простые степени произведение распадается по простым: базовые значения в произведении по p и вложенное произведение по степеням выше, давая разложение по простым множителям.
LaTeX
$$$\prod_{n} f(n) = (\prod_{p\in\text{Primes}} f(p)) \cdot \prod_{p\in\text{Primes}} \prod_{k\ge 0} f(p^{(k+2)})$$$
Lean4
@[to_additive tsum_eq_tsum_primes_add_tsum_primes_of_support_subset_prime_powers]
theorem tprod_eq_tprod_primes_mul_tprod_primes_of_mulSupport_subset_prime_powers {f : ℕ → α} (hfm : Multipliable f)
(hf : Function.mulSupport f ⊆ {n | IsPrimePow n}) :
∏' n : ℕ, f n = (∏' p : Nat.Primes, f p) * ∏' (p : Nat.Primes) (k : ℕ), f (p ^ (k + 2)) :=
by
rw [tprod_eq_tprod_primes_of_mulSupport_subset_prime_powers hfm hf]
have hfs' (p : Nat.Primes) : Multipliable fun k : ℕ ↦ f (p ^ (k + 1)) :=
hfm.comp_injective <|
(strictMono_nat_of_lt_succ fun k ↦ pow_lt_pow_right₀ p.prop.one_lt <| lt_add_one (k + 1)).injective
conv_lhs =>
enter [1, p]; rw [(hfs' p).tprod_eq_zero_mul, zero_add, pow_one]
enter [2, 1, k]; rw [add_assoc, one_add_one_eq_two]
exact
(Multipliable.subtype hfm _).tprod_mul <|
Multipliable.prod (f := fun (pk : Nat.Primes × ℕ) ↦ f (pk.1 ^ (pk.2 + 2))) <|
hfm.comp_injective <|
Subtype.val_injective |>.comp Nat.Primes.prodNatEquiv.injective |>.comp <|
Function.Injective.prodMap (fun ⦃_ _⦄ a ↦ a) <| add_left_injective 1
