Computing finset (range) sums

Stream: new members

[Pedro Minicz]

How to deal with computations on finite sets?

import algebra.big_operators
import data.real.ennreal

open_locale big_operators

def f (n : ℕ) : ℝ := if n < 2 then 1 else 0

example : ∑ i in finset.range 0, f i = 0 :=
by refl -- or `simp only [finset.sum_empty, finset.range_zero]`

example : ∑ i in finset.range 1, f i = 1 :=
by simp [f, finset.sum_singleton]

example : ∑ i in finset.range 2, f i = 2 :=
sorry

example (n : ℕ) : ∑ i in finset.range n, f i < n + 1 :=
sorry

I think the examples above motivate the question quite well. Its pretty easy to deal with summations on the empty set or singleton sets thanks to the lemmas sum_empty and sum_singleton, however I am unable to proof anything past 2.

[Pedro Minicz]

It should be possible to be able to proof the last example by induction on n, I believe.

[Jalex Stark]

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators.html#finset.sum_range_succ

[Jalex Stark]

https://leanprover-community.github.io/mathlib_docs/algebra/big_operators.html#finset.sum_range_induction

[Pedro Minicz]

Hmm, it was on algebra. I looked for this on finset. :innocent:

[Bhavik Mehta]

I think a few people have been caught out by this (myself included), I wonder if it's a good idea to put a note somewhere in finset saying that these lemmas are in algebra not in finset

[Bryan Gin-ge Chen]

data.finset is missing a ton of documentation. A PR would be greatly appreciated!

[Jalex Stark]

if you want to not be caught out like this in the future, use the "right click -> go to definition" and "right click -> peek definition" in VSCode

[Jalex Stark]

or search the name of a lemma (like finset.sum_singleton) in the mathlib docs

[Kevin Buzzard]

Docstring PR's are really easy to make and teach you a lot about the library. I needed to learn about multivariable polynomials so I wrote the module docstring for the relevant Lean file. You just have to isolate the definitions and explain them at the top, and follow the style guide which is in the docs directory of mathlib.

[Bhavik Mehta]

Jalex Stark said:

if you want to not be caught out like this in the future, use the "right click -> go to definition" and "right click -> peek definition" in VSCode

I don't think this helps in this case, since the lemmas are defined in algebra and not referenced anywhere in finset, so if you're in finset you wouldn't be able to chase definitions to algebra.big_ops

[Jalex Stark]

i thought the problem is "i know about finset.sum_singleton but not about other lemmas in big_operators"?

[Bhavik Mehta]

Oh, my mistake, you're right!

[Pedro Minicz]

Jalex Stark said:

i thought the problem is "i know about finset.sum_singleton but not about other lemmas in big_operators"?

I've been jumping to definitions all the time in VSCode and honestly didn't even notice finset.sum_singleton was in algebra.

[Pedro Minicz]

I guess I could have payed more attention. :upside_down:

[Jalex Stark]

without knowing the name of the file, if your goal is "find functions like finset.sum_singleton", then the tactic "look nearby in the file defining finset.sum_singleton" makes significant progress