[Merged by Bors] - feat: Sedrakyan's lemma

[vihdzp]

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 [email protected]
Co-authored-by: Heather Macbeth [email protected]

---

[github-actions]

PR summary a0fa1f1309

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ sq_sum_div_le_sum_sq_div
+ sum_sq_le_sum_mul_sum_of_sq_eq_mul
+ two_mul_le_add_of_sq_eq_mul

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[eric-wieser]

Orthogonal to my question above, I wonder if we want the "generalized form" from https://brilliant.org/wiki/titus-lemma/#generalized-form as well.

[vihdzp]

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]

Thanks! Looks like a great improvement over the original version

[YaelDillies]

Can you move this out of the LinearOrderedCommSemiring section?

[vihdzp]

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.

[vihdzp]

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).

[vihdzp]

I've reordered the file slightly, does this change make sense?

[eric-wieser]

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.

[vihdzp]

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".

[YaelDillies]

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

[eric-wieser]

bors d=@YaelDillies

Thanks, this now looks great!

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style