## 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

#### 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: May 13 2021 at 00:41 UTC