Dirichlet convolution

Stream: maths

[Elliott Macneil]

I'm trying to define the Dirichlet convolution on two arithmetic functions f,g but I'm having difficulty with writing the following sum in Lean.

$\Sigma_{d \mid n } f(d) g(n/d)$

Could anyone possibly write this in Lean?

[Kevin Buzzard]

Elliott I pushed a function which did this this morning.

[Kevin Buzzard]

What does this mean if n=0?

[Kevin Buzzard]

I stuck to pnat

[Kevin Buzzard]

https://github.com/ImperialCollegeLondon/xena-UROP-2018/blob/master/src/M3P14/sum_over_divisors.lean

[Kevin Buzzard]

so it's \lam (n : pnat), divisor_sum (\lam d, f d * g (n / d)) n

[Mario Carneiro]

lemma mem_factors_iff_divides (d : ℕ+) (e : ℕ) : e ∈ factors d ↔ e ∣ d :=
by simp [factors, -add_comm, nat.lt_succ_iff];
   exact and_iff_right_of_imp (le_of_dvd d.2)

[Mario Carneiro]

see, logic.basic is useful

[Mario Carneiro]

you can also define factors using finset.filter to avoid the nodup proof

[Kevin Buzzard]

Thanks and thanks! I was surprised that the divisors function (sending a pnat to a finset of its divisors) wasn't there, but Chris said he hadn't seen it (he had seen factors which in my mind is synonymous, however he said factors was the list of prime factors of n, which is not how the word is usually used in mathematics: factor does not imply prime).

[Mario Carneiro]

I had the same train of thought

[Mario Carneiro]

maybe it should be called factorization

[Mario Carneiro]

note that it is not just the set of prime factors, it is like a multiset

[Kevin Buzzard]

I should use simp for iff statements more...

[Elliott Macneil]

Thanks for the help!