[Merged by Bors] - feat(analysis/mean_inequalities): add Minkowski's inequality for the Lebesgue integral of ennreal functions

[RemyDegenne]

---

I am not happy with the private lemma named minkowski_aux but it proves something so specific and unlikely to be used elsewhere that I opted for not giving it a descriptive (and convoluted) name.

[sgouezel]

I am not so sure that the lemma should be private, you never know what might be handy later on. A name like lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow would be fine for me. On the other hand, I wouldn't mind at all if you make the lemma lintegral_rpow_add_le_add_lintegral_rpow_of_lintegral_add_ne_zero_ne_top private and replaced its name with lintegral_rpow_add_le_add_lintegral_rpow_aux: the assumptions of this lemma are strictly stronger than the ones in lintegral_rpow_add_le_add_lintegral_rpow, so there is no situation where it could be useful later on.

Also, the name for finite sums is Lp_add_le, which is both short and to the point. What about finding a short name also for the integral version? I think I would even advocate Lp_add_le for the integral version, and Lp_sum_add_le for the finite version. Except that other versions are coming, so maybe lintegral_Lp_add_le for the current integral version?

[RemyDegenne]

I changed the names and private status:

• the lemma that was private isn't anymore, and is now called lintegral_mul_rpow_le_lintegral_rpow_mul_lintegral_rpow.
• the lemma that proves Minkowski's inequality under stronger assumptions is now private, and called lintegral_Lp_add_le_aux,
• Minkowski's inequality is now lintegral_Lp_add_le

[sgouezel]

bors r+
Thanks!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Run tests
• Lint mathlib
• Build mathlib