Zulip Chat Archive

Is there something somewhat between list.sum and finset.sum - I'm looking to work with a sum over [0..k] (and ideally induct on k). I know I could use list.sum (list.map f) (range n), but since finset.sum takes an extra mapping parameter I was wondering if there's a version of list.sum with this extra parameter as well

Johan Commelin (Dec 04 2019 at 12:22):

Why would finset.sum not work?

Bhavik Mehta (Dec 04 2019 at 12:22):

Oh. That's a good point. Thanks!

Luis O'Shea (Dec 04 2019 at 23:10):

When working with finite sums I have used list.sum and list.range. However it seems that finset is the preferred way (e.g., Gauss' summation formula in mathlib). What are the advantages of finset over list for this use?

Bhavik Mehta (Dec 04 2019 at 23:12):

One advantage is the use-case I mentioned above, where we want to sum a function over a range, rather than just sum over a set (without the indirection of map)

Bryan Gin-ge Chen (Dec 04 2019 at 23:22):

I think the main advantage is just that finset.sum has a lot more theorems proved about it. I don't know (but would like to know) whether it would be possible / desirable to prove them all for multiset.sum and list.sum.

Luis O'Shea (Dec 04 2019 at 23:45):

@Bryan Gin-ge Chen that makes sense. However I now have a very basic question. It took me a long time to find finset.sum (by trial and error import data.fintype worked; in particular import data.finset is not enough). Is there a better way than trial and error?

Bryan Gin-ge Chen (Dec 04 2019 at 23:52):

Good question. For some reason all those definitions are in algebra.big_operators. I'm not sure of the best way of finding that out if you're new.

Mario Carneiro (Dec 05 2019 at 00:06):

The reason list.sum doesn't have a function argument is exactly because you can apply list.map first. You can't do this for finset.sum because mapping a finset to another finset will cause duplicates to be removed

Mario Carneiro (Dec 05 2019 at 00:11):

algebra.big_operators is kind of in a weird position because it is the dependency sup of finset and the algebra collection. We don't really want either of those to import the other, but then stuff depending on both gets orphaned

Luis O'Shea (Dec 05 2019 at 00:17):

From a practical perspective I suspect that @Bryan Gin-ge Chen's point ("a lot more theorems") makes finset.sum the natural choice. However, philosophically is list.sum closer to what mathematicians mean? For example it would not be particularly strange to see something like $\sum_{i=1,2,2,3,3,3} f(n)$ in a mathematical paper. (Perhaps I should take a look at those theorems and see whether they apply to list.)

Mario Carneiro (Dec 05 2019 at 00:22):

For example it would not be particularly strange to see something like $\sum_{i=1,2,2,3,3,3} f(n)$ in a mathematical paper.

I would find that very strange, but perhaps that's another matter.

Mario Carneiro (Dec 05 2019 at 00:23):

I would think $f(1)+2f(2)+3f(3)$ would be more likely

Bhavik Mehta (Dec 05 2019 at 00:40):

I agree that list.sum feels closer to what's intended, which was the idea behind the original question here

Kevin Buzzard (Dec 05 2019 at 01:37):

Bryan Gin-ge Chen that makes sense. However I now have a very basic question. It took me a long time to find finset.sum (by trial and error import data.fintype worked; in particular import data.finset is not enough). Is there a better way than trial and error?

Yes. Ask here! Alternatively go to VS Code and search for finset.sum. If you get only a few results, you are not searching in mathlib and you have to fiddle with your settings.

Kevin Buzzard (Dec 05 2019 at 01:39):

I get 306 results for finset.sum. "Search mathlib" is off by default for new VS Code projects for me. It's a real pain. I've had to show several Imperial UG's how to search mathlib because the magnifying glass sometimes doesn't work by default.

Alex J. Best (Dec 05 2019 at 01:41):

Is there a recommended option for "search mathib"? I've been adding ./_target/deps/**/*.* to the "files to include" box to have this work, would be nice if there was an option for the vscode extension?

Kevin Buzzard (Dec 05 2019 at 01:42):

If your code has mathlib as a dependency then there's a sometimes very well-hidden cog with a small minus sign on it ("exclude settings files").

Kevin Buzzard (Dec 05 2019 at 01:43):

search.png

Kevin Buzzard (Dec 05 2019 at 01:44):

If it's light blue (i.e. on), click on it. Then VS Code search will look in mathlib.

Alex J. Best (Dec 05 2019 at 01:48):

Nice, thanks!

Luis O'Shea (Dec 05 2019 at 02:45):

@Kevin Buzzard's suggestion worked (namely, clicking on the little cog at the right end of the "files to include" box) -- thanks! For other beginners (like me), after you click on a search result you may need to wait a while until Lean parses the file (completely?) to get "go to definition" to work. Once it does, it works great (and, indeed, took me to big_operators.lean).

Bhavik Mehta (Dec 05 2019 at 11:34):