[Merged by Bors] - feat(analysis/mean_inequalities): Holder and Minkowski inequalities

[urkud]

---

Golfing proofs for @sgouezel's #2988. Dep: #3023.

@sgouezel Do you prefer to move proofs to your PR or comments to this one?

[jcommelin]

@urkud What is the correct transliteration “Minkowski” or “Minkowskii”?

[urkud]

@urkud What is the correct transliteration “Minkowski” or “Minkowskii”?

It's Minkowski in all sources, so the correct transliteration is Minkowski. I suspect that this was the transliteration he used when he was alive. Sorry for the confusion.

P.S.: There is no unique "correct" transliteration. E.g., transliteration rules used by Russian government to transliterate names in passports were changed many times. My 3 passports have 3 different transliterations of my name.

[digama0]

ий is usually transliterated as "i" or "iy", but from what I can tell Hermann Minkowski, Polish by birth, never used Cyrillic for his name, and wrote his name "Minkowski" while living in Germany.

[urkud]

It's possible that his parents used Cyrillic in some documents (Poland was a part of Russian empire). I don't know.

[jcommelin]

Thanks. I updated the PR title.

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Run tests and docs
• Build mathlib