bounding a \sum with a single element — where do I put this?

Stream: maths

[Jakub Kądziołka]

I found myself having to use this often enough to extract a lemma. Where in mathlib should I put it?

lemma sum_gt_element {f : ℕ → ℕ} {S : finset ℕ} {n : ℕ} (Hn : n ∈ S): S.sum f ≥ f n :=
begin
  calc S.sum f = (insert n (S.erase n)).sum f : by rwa finset.insert_erase
  ...          ≥ f n                          : by simp
end

[Alex J. Best]

algebra/big_operators/basic.lean seems fine, but if it goes in mathlib it should:

• use le instead of ge
• be generalized to be about prod and have the sum version generated with to_additive
• be generalized to more general types than nat to nat where possible
• if the proof is just a calc you don't need begin... end
• be called something like le_prod_of_mem

[Jakub Kądziołka]

how do you generalize this to prod? it doesn't work for prod because other terms might be zero

[Jakub Kądziołka]

is there a typeclass for "ordered type where only 0 has an additive inverse"?

[Ruben Van de Velde]

Ordered semiring, maybe?

[Alex J. Best]

You're only using addition here so there shouldn't be an issue, you just have 1's instead of zeroes.
Things like docs#fintype.prod_eq_prod_compl_mul in the file I mentioned are really close to this

[Rémy Degenne]

your lemma looks like docs#finset.single_le_sum specialized to N

[Jakub Kądziołka]

Rémy Degenne said:

your lemma looks like docs#finset.single_le_sum specialized to N

Do you just know this lemma, or did you find it with some query?

[Mario Carneiro]

It is located where you would expect theorems about ordering and bigops to be, so one way to find this theorem is to open the file (in src or docgen) and browse around

[Mario Carneiro]

Note that you would have to do this eventually anyway when deciding where to put your theorem

[Rémy Degenne]

I guessed that it should be a name involving le_sum and searched for that in the doc. Then I saw a name of a lemma which sounded similar but was not exactly the one I looked for, looked around a bit in the file and found it

[Rémy Degenne]

I did not guess the word single because that's not a very frequent one

[Jakub Kądziołka]

okay. I'm asking because in Isabelle I'd do find_theorems "_ \in _" "_ <= \sum _"

[Mario Carneiro]

You can use #find and tactic#library_search for that kind of search

[Jakub Kądziołka]

don't I need the full type of the theorem for #find (which itself may contain holes)?

[Mario Carneiro]

I don't think so? It should be looking for the term as a subterm of the theorem statement

[Mario Carneiro]

You can also use text search btw

[Jakub Kądziołka]

ah, looks like you're right. How can I provide multiple patterns? , terminates the entire command

[Mario Carneiro]

I don't think you can

[Mario Carneiro]

the situation is not that great, I will admit. Most people seem to find library_search the most helpful, and I usually use a combination of autocomplete and browsing in files

[Mario Carneiro]

it helps a lot to learn the naming convention

[Mario Carneiro]

it is not unusual to be able to guess a name exactly, or stumble on the theorem you wanted by a redeclaration error