Commit 2024-01-10 14:23 d819f3c8

View on Github →

feat: Maximum principle for convex functions on an interval (#9364) Corollaries of existing lemmas. From LeanAPAP

Estimated changes

Modified Mathlib/Analysis/Convex/Jensen.lean

added theorem ConcaveOn.min_le_of_mem_Icc

added theorem ConcaveOn.min_le_of_mem_segment

added theorem ConvexOn.le_max_of_mem_Icc

added theorem ConvexOn.le_max_of_mem_segment