## Stream: maths

### Topic: Dirichlet convolution

#### Elliott Macneil (Aug 15 2018 at 15:43):

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 (Aug 15 2018 at 15:46):

Elliott I pushed a function which did this this morning.

#### Kevin Buzzard (Aug 15 2018 at 15:46):

What does this mean if n=0?

#### Kevin Buzzard (Aug 15 2018 at 15:47):

I stuck to pnat

#### Kevin Buzzard (Aug 15 2018 at 15:47):

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

#### Kevin Buzzard (Aug 15 2018 at 15:49):

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

#### Mario Carneiro (Aug 15 2018 at 15:51):

lemma mem_factors_iff_divides (d : ℕ+) (e : ℕ) : e ∈ factors d ↔ e ∣ d :=
exact and_iff_right_of_imp (le_of_dvd d.2)


#### Mario Carneiro (Aug 15 2018 at 15:52):

see, logic.basic is useful

#### Mario Carneiro (Aug 15 2018 at 15:53):

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

#### Kevin Buzzard (Aug 15 2018 at 16:45):

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 (Aug 15 2018 at 16:49):

I had the same train of thought

#### Mario Carneiro (Aug 15 2018 at 16:50):

maybe it should be called factorization

#### Mario Carneiro (Aug 15 2018 at 16:51):

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

#### Kevin Buzzard (Aug 15 2018 at 16:53):

I should use simp for iff statements more...

#### Elliott Macneil (Aug 15 2018 at 18:37):

Thanks for the help!

Last updated: May 12 2021 at 07:17 UTC