Commit 2023-04-24 21:46 4929c76a

View on Github →

feat: port Analysis.Convex.Jensen (#3622)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Jensen.lean

added theorem ConcaveOn.exists_le_of_centerMass

added theorem ConcaveOn.exists_le_of_mem_convexHull

added theorem ConcaveOn.le_map_centerMass

added theorem ConcaveOn.le_map_sum

added theorem ConvexOn.exists_ge_of_centerMass

added theorem ConvexOn.exists_ge_of_mem_convexHull

added theorem ConvexOn.map_centerMass_le

added theorem ConvexOn.map_sum_le

added theorem inf_le_of_mem_convexHull

added theorem le_sup_of_mem_convexHull