Zulip Chat Archive

Stream: new members

Topic: max vs sum?


view this post on Zulip Alex Kontorovich (Oct 23 2020 at 22:14):

Hello, can someone please help me properly state (and prove) the following: If S is a finite set of nonnegative reals, then the sum over S is at most the cardinality times the largest? Thanks!

lemma max_lemma (S : finset 0 ) :
  S.sum   S.cardinality * (Sup S) :=
begin
end

view this post on Zulip Kevin Lacker (Oct 23 2020 at 22:17):

try inducting on the cardinality

view this post on Zulip Adam Topaz (Oct 23 2020 at 22:19):

Or on the finset itself, e.g. using docs#finset.induction / docs#finset.induction_on

view this post on Zulip Heather Macbeth (Oct 23 2020 at 22:19):

I think there are pre-existing lemmas that should avoid an explicit induction. Like docs#finset.sum_const

view this post on Zulip Heather Macbeth (Oct 23 2020 at 22:20):

And docs#finset.sum_le_sum

view this post on Zulip Alex Kontorovich (Oct 23 2020 at 22:24):

(Is it cheating if you help me with my own "homework"?..) :)

view this post on Zulip Kevin Lacker (Oct 23 2020 at 22:37):

see heather is helping you cheat, by giving you good advice. if you follow my mediocre advice, it work, but it will probably take even longer than if you figured it out by yourself

view this post on Zulip Bryan Gin-ge Chen (Oct 23 2020 at 22:50):

I can confirm that Heather's advice is good, in that it leads to a 2-line proof (or shorter?) of the following:

import data.real.nnreal

open_locale big_operators nnreal

lemma max_lemma (S : finset 0) (hS : S.nonempty) :
  ( s in S, s : 0)  S.card * (S.max' hS) :=
begin
  sorry,
end

Last updated: May 13 2021 at 00:41 UTC