[Merged by Bors] - feat: Sedrakyan's lemma#19311
Conversation
PR summary a0fa1f1309Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
Orthogonal to my question above, I wonder if we want the "generalized form" from https://brilliant.org/wiki/titus-lemma/#generalized-form as well. |
|
I didn't even know there was a generalized form! I think we can add it later if it ever becomes useful for anything. |
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! Looks like a great improvement over the original version
|
|
||
| This is a specialization of the Cauchy-Schwarz inequality with the sequences `f n / √(g n)` and | ||
| `√(g n)`, though here it is proven without relying on square roots. -/ | ||
| theorem sq_sum_div_le_sum_sq_div [LinearOrderedSemifield R] [ExistsAddOfLE R] (s : Finset ι) |
There was a problem hiding this comment.
Can you move this out of the LinearOrderedCommSemiring section?
There was a problem hiding this comment.
This theorem is right after the end of that section. I didn't think it'd make sense to make a new section for just this one theorem.
There was a problem hiding this comment.
Actually, I think it makes more sense to just have a "named inequalities" section in the file. (I also want to add Nesbitt in a subsequent PR, which can be proven as a consequence of Sedrakyan).
There was a problem hiding this comment.
I've reordered the file slightly, does this change make sense?
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
| /-! ### Named inequalities -/ | ||
|
|
There was a problem hiding this comment.
I suspect this grouping isn't particularly helpful in the long term, because inevitably it ends up being desirable to extract a helper lemma that sits between these. I'll let @YaelDillies decide though.
There was a problem hiding this comment.
Fair, this wasn't meant so much as a "inequalities with names go here" but rather as a "the more difficult and mathematically interesting results go here".
There was a problem hiding this comment.
I suspect it will change again once we add the inequalities you both mentioned, but until then this looks like a mostly okay sectioning.
bors merge
|
bors d=@YaelDillies Thanks, this now looks great! |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
This is a specialization of the Cauchy-Schwarz inequality which is often useful in math olympiad problems. In order to prove it in general ordered semifields, we have to show slightly more general forms of the AM-GM and Cauchy-Schwarz inequalities, which indirectly work with square roots. Co-authored-by: Alex Brodbelt <64128135+AlexBrodbelt@users.noreply.github.com> Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com>
|
Pull request successfully merged into master. Build succeeded: |
This is a specialization of the Cauchy-Schwarz inequality which is often useful in math olympiad problems.
In order to prove it in general ordered semifields, we have to show slightly more general forms of the AM-GM and Cauchy-Schwarz inequalities, which indirectly work with square roots.
Co-authored-by: Alex Brodbelt 64128135+AlexBrodbelt@users.noreply.github.com
Co-authored-by: Heather Macbeth 25316162+hrmacbeth@users.noreply.github.com