Zulip Chat Archive

Stream: maths

Topic: Sums over finsets


view this post on Zulip Johan Commelin (May 22 2018 at 14:09):

I'm stuck on the following triviality

lemma sums {m n : } (f : fin m  fin n) (x : fin m  )
: sum univ (λ j : fin n, sum (univ.filter (λ i, f i = j)) x) = sum univ x
:= sorry

It looks like I might want to use finset.sum_sigma but I don't see how to get all the sigma's in place. And the unification magic doesn't do the job either.

view this post on Zulip Johan Commelin (May 22 2018 at 14:10):

@Kevin Buzzard @Chris Hughes I remember that you were also working on these kind of sum-rewritings about 2 months ago. Is this similar to what you did?

view this post on Zulip Johannes Hölzl (May 22 2018 at 14:18):

you can use finset.sum_bind to combine both sum to a single one and then use extensionality that the combination of the index sets on the right is univ. Or use finset.sum_subset which also uses some sort of extensionality.

view this post on Zulip Johan Commelin (May 22 2018 at 14:28):

Ok, thanks!

view this post on Zulip Johan Commelin (May 22 2018 at 17:20):

Ok, I proved the lemma using bind and ext.2. Thanks a lot!


Last updated: May 11 2021 at 15:12 UTC