English
Let f be an arithmetic function with values in a semiring R. Then for every natural number x, the Dirichlet convolution of f with the divisor zeta function ζ satisfies (f * ζ)(x) = sum_{d | x} f(d). The divisor zeta function ζ assigns 1 to every positive integer, and the convolution sums f over all divisors of x.
Русский
Пусть f — арифметическая функция со значениями в полукольце R. Тогда для каждого натурального числа x Дирихлева свёртка f с делителями ζ удовлетворяет (f * ζ)(x) = ∑_{d | x} f(d). Делительская ζ задаёт значения 1 для всех положительных целых, и свёртка суммирует значения f по всем делителям x.
LaTeX
$$$$ (f * \zeta)(x) = \sum_{d \mid x} f(d) $$$$
Lean4
theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (f * ζ) x = ∑ i ∈ divisors x, f i :=
by
rw [mul_apply]
trans ∑ i ∈ divisorsAntidiagonal x, f i.1
· refine sum_congr rfl fun i hi => ?_
rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩
rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one]
· rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk]
