max vs sum?

Stream: new members

[Alex Kontorovich]

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]

try inducting on the cardinality

[Adam Topaz]

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

[Heather Macbeth]

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

[Heather Macbeth]

And docs#finset.sum_le_sum

[Alex Kontorovich]

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

[Kevin Lacker]

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]

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