Zulip Chat Archive

Stream: maths

Topic: sigma


Guy Leroy (Aug 01 2018 at 15:47):

Does anyone know how hard it would be to implement the sigma sum in Lean?

Johan Commelin (Aug 01 2018 at 15:47):

As in, big operators?

Guy Leroy (Aug 01 2018 at 15:48):

As in summing the numbers from 1 to n

Guy Leroy (Aug 01 2018 at 15:48):

and ideally summing over the elements of a set

Johan Commelin (Aug 01 2018 at 15:50):

There is a big_operators.lean file.

Johan Commelin (Aug 01 2018 at 15:50):

In algebra/

Johan Commelin (Aug 01 2018 at 15:51):

And I think Patrick has a project that is causing him royal pains. But it should allow for easier handling of these beasts.

Kevin Buzzard (Aug 01 2018 at 15:53):

I think @Chris Hughes might have also done some stuff with this. It's a good question! To answer an M1F question I needed to prove that Σi=1nai=Σj=1nan+1j\Sigma_{i=1}^na_i=\Sigma_{j=1}^na_{n+1-j} and I don't think I ever managed to do this; I think Mario explained a technique which would have worked but I never got around to implementing it. I'd like to see basic facts about series manipulation all in some library, and if it's a bit too low-brow for mathlib we could put it in Xena's library.


Last updated: Dec 20 2023 at 11:08 UTC