Commit 2022-09-13 13:37 01a8a9f8
View on Github →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.