mathlib

81e58c9e - feat(analysis/mean_inequalities): corollary of Hölder inequality (#10789)

feat(analysis/mean_inequalities): corollary of Hölder inequality (#10789) Several versions of the fact that ``` (∑ i in s, f i) ^ p ≤ (card s) ^ (p - 1) * ∑ i in s, (f i) ^ p ``` for `1 ≤ p`.