The divisor multiplication table of a prime-power-multiplicative family

Fix a commutative semiring R and two block maps D S : ℕ → ℕ → R, and assemble each over a prime factorisation with TauCeti.Nat.primePowerProd. Suppose the assembled D obeys the per-prime table: for a prime p and r ≤ s,

D_{p^r} · D_{p^s} = ∑_{i ≤ r} pⁱ • (S_{pⁱ} · D_{p^{r+s−2i}}).

Then it obeys the global one, over every pair of nonzero arguments at once:

D_m · D_n = ∑_{d ∣ gcd m n} d • (S_d · D_{mn/d²}).

Main results

• TauCeti.Nat.primePowerProd_mul_eq_sum_divisors_gcd: the global table, deduced from the per-prime one.

The scalars are natural numbers and no subtraction occurs, so a commutative semiring is enough; the Hecke-ring consumer is a ring and converts to its ℤ-scalars at the point of use.

Relation to Mathlib

Mathlib's ArithmeticFunction.IsMultiplicative describes families multiplicative on coprime arguments, and ArithmeticFunction.mul gives them a Dirichlet convolution. Neither expresses this table: the right-hand side is not a convolution of two arithmetic functions — the index mn/d² is quadratic in the divisor, and the S-factor is evaluated at d while the D-factor is evaluated at mn/d². The statement is also not about a function ℕ → R but about the assembled family, so the per-prime table is the input rather than multiplicativity.

References

• G. Shimura, Introduction to the arithmetic theory of automorphic functions, §3.3 — Theorem 3.24, whose Hecke-ring instance is the intended consumer.
• Ported from AINTLIB, Apache-2.0, Chris Birkbeck, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Unified/Gamma0RingDn.lean, section FormalTable (lines 186-438). Two differences in the statement: the sum is taken over Nat.divisors rather than its Finset.attach, the summand never inspecting a membership proof, and the index is d ^ 2 rather than the source's d * d. The source's peelProd is this repository's TauCeti.Nat.primePowerProd, and the gcd splitting it needs is TauCeti.Data.Nat.Factorization.GcdSplit.

The table

theorem TauCeti.Nat.primePowerProd_mul_eq_sum_divisors_gcd {R : Type u_1} [CommSemiring R] (D S : ℕ → ℕ → R) (hppow : ∀ (p : ℕ), Nat.Prime p → ∀ (r s : ℕ), r ≤ s → primePowerProd D (p ^ r) * primePowerProd D (p ^ s) = ∑ i ∈ Finset.range (r + 1), p ^ i • (primePowerProd S (p ^ i) * primePowerProd D (p ^ (r + s - 2 * i)))) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) : primePowerProd D m * primePowerProd D n = ∑ d ∈ (m.gcd n).divisors, d • (primePowerProd S d * primePowerProd D (m * n / d ^ 2))

The divisor multiplication table. A family assembled over prime factorisations obeying the per-prime table D_{p^r}·D_{p^s} = ∑_{i ≤ r} pⁱ • (S_{pⁱ}·D_{p^{r+s−2i}}) obeys the global one

D_m · D_n = ∑_{d ∣ gcd m n} d • (S_d · D_{mn/d²}).

Both arguments must be nonzero: primePowerProd sends 0 to the empty product, and gcd 0 0 = 0 has no divisors, so at m = n = 0 the left side is 1 and the right an empty sum.