mathlib3

8a13846e - feat(analysis/mean_inequalities): Hölder's inequality for infinite sums (#11314)

feat(analysis/mean_inequalities): Hölder's inequality for infinite sums (#11314) State a few versions of Hölder's inequality for infinite sums. The specific forms of the inequality chosen are parallel to those for Minkowski's inequality in #10984.