mathlib3

01a8a9f8 - feat(convex/specific_functions): specific case of Jensen's inequality for powers (#16186)

feat(convex/specific_functions): specific case of Jensen's inequality for powers (#16186) Proves a specific case of Jensen's inequality: a powers of a sum divided by the cardinality of the `finset` is less than or equal to the sum of the powers.