# Zulip Chat Archive

## 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 := by simp [factors, -add_comm, nat.lt_succ_iff]; 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