Zulip Chat Archive

Stream: new members

Topic: sum of inequalities of functions


view this post on Zulip Kyle Miller (Sep 10 2020 at 02:27):

What's the best way to fill in this sorry?

import data.fintype.basic
import algebra.big_operators

open_locale big_operators

example {α : Type*} [fintype α] (f : α  ) (g : α  ) (h :  a, f a  g a) :
   a, f a   a, g a :=
begin
  sorry,
end

view this post on Zulip Johan Commelin (Sep 10 2020 at 02:29):

I think there is finset.sum_le_sum

view this post on Zulip Alex J. Best (Sep 10 2020 at 02:32):

example {α : Type*} [fintype α] (f : α  ) (g : α  ) (h :  a, f a  g a) :
   a, f a   a, g a :=  finset.sum_le_sum (λ x _ , h x)

view this post on Zulip Bryan Gin-ge Chen (Sep 10 2020 at 02:33):

How well does suggest do with this?

view this post on Zulip Alex J. Best (Sep 10 2020 at 02:34):

Not so well when I tried it, I didn't see anything useful from a quick look anyway.

view this post on Zulip Kyle Miller (Sep 10 2020 at 02:35):

I was editing things in algebra.big_operators.basic itself, so I wasn't able to see it with either library_search or suggest

view this post on Zulip Kyle Miller (Sep 10 2020 at 02:35):

Thanks for pointing me to it!

view this post on Zulip Alex J. Best (Sep 10 2020 at 02:36):

At least for me library search and suggest didn't work, I had to fall back to the old trusty of guess the name of a useful lemma!

view this post on Zulip Kenny Lau (Sep 10 2020 at 06:11):

kids these days with their suggest tactics


Last updated: May 13 2021 at 21:12 UTC