-
Notifications
You must be signed in to change notification settings - Fork 298
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(analysis/mean_inequalities) : Prove AM-GM #1836
Conversation
open real finset | ||
open_locale classical nnreal | ||
|
||
variables {ι : Type u} (s : finset ι) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
s
could be implicit in most statements (all?)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
When I specialize the theorems for 2 and 3 variables I explicitly supply univ
because I have w₁+w₂=1
, not univ.sum w = 1
.
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-Authored-By: Johan Commelin <johan@commelin.net>
…1836) * feat(analysis/mean_inequalities) : Prove AM-GM * Update, add more inequalities * Update src/analysis/convex/specific_functions.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Update src/analysis/mean_inequalities.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Update src/analysis/mean_inequalities.lean * Small fixes, thanks @sgouezel * Update src/analysis/mean_inequalities.lean Co-Authored-By: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
…1836) * feat(analysis/mean_inequalities) : Prove AM-GM * Update, add more inequalities * Update src/analysis/convex/specific_functions.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Update src/analysis/mean_inequalities.lean Co-Authored-By: sgouezel <sebastien.gouezel@univ-rennes1.fr> * Update src/analysis/mean_inequalities.lean * Small fixes, thanks @sgouezel * Update src/analysis/mean_inequalities.lean Co-Authored-By: Johan Commelin <johan@commelin.net> Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Should be ready now. I can't guess what versions will be useful in practice, so I prove a few versions, and leave the rest to someone who'll want to actually use these inequalities.