Zulip Chat Archive

Stream: maths

Topic: Dirichlet convolution


view this post on Zulip 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.

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

Could anyone possibly write this in Lean?

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 15:46):

Elliott I pushed a function which did this this morning.

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 15:46):

What does this mean if n=0?

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 15:47):

I stuck to pnat

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 15:47):

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

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 15:49):

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

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Aug 15 2018 at 15:52):

see, logic.basic is useful

view this post on Zulip Mario Carneiro (Aug 15 2018 at 15:53):

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

view this post on Zulip 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).

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:49):

I had the same train of thought

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:50):

maybe it should be called factorization

view this post on Zulip Mario Carneiro (Aug 15 2018 at 16:51):

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

view this post on Zulip Kevin Buzzard (Aug 15 2018 at 16:53):

I should use simp for iff statements more...

view this post on Zulip Elliott Macneil (Aug 15 2018 at 18:37):

Thanks for the help!


Last updated: May 12 2021 at 07:17 UTC