sigma

Stream: maths

[Guy Leroy]

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

[Johan Commelin]

As in, big operators?

[Guy Leroy]

As in summing the numbers from 1 to n

[Guy Leroy]

and ideally summing over the elements of a set

[Johan Commelin]

There is a big_operators.lean file.

[Johan Commelin]

In algebra/

[Johan Commelin]

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]

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 $\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.