Zulip Chat Archive

Stream: new members

Topic: max vs sum?


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

Kevin Lacker (Oct 23 2020 at 22:17):

try inducting on the cardinality

Adam Topaz (Oct 23 2020 at 22:19):

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

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

Heather Macbeth (Oct 23 2020 at 22:20):

And docs#finset.sum_le_sum

Alex Kontorovich (Oct 23 2020 at 22:24):

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

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

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: Dec 20 2023 at 11:08 UTC