Commit 2023-04-10 15:18 16371bdd

View on Github →

feat: port Analysis.Convex.Function (#3152)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Function.lean

added theorem ConcaveOn.add

added theorem ConcaveOn.add_strictConcaveOn

added theorem ConcaveOn.comp

added theorem ConcaveOn.comp_affineMap

added theorem ConcaveOn.comp_convexOn

added theorem ConcaveOn.comp_linearMap

added theorem ConcaveOn.convex_ge

added theorem ConcaveOn.convex_gt

added theorem ConcaveOn.convex_hypograph

added theorem ConcaveOn.convex_strict_hypograph

added theorem ConcaveOn.dual

added theorem ConcaveOn.ge_on_segment'

added theorem ConcaveOn.ge_on_segment

added theorem ConcaveOn.inf

added theorem ConcaveOn.left_le_of_le_right''

added theorem ConcaveOn.left_le_of_le_right'

added theorem ConcaveOn.left_le_of_le_right

added theorem ConcaveOn.left_lt_of_lt_right'

added theorem ConcaveOn.left_lt_of_lt_right

added theorem ConcaveOn.lt_right_of_left_lt'

added theorem ConcaveOn.lt_right_of_left_lt

added theorem ConcaveOn.openSegment_subset_strict_hypograph

added theorem ConcaveOn.right_le_of_le_left''

added theorem ConcaveOn.right_le_of_le_left'

added theorem ConcaveOn.right_le_of_le_left

added theorem ConcaveOn.smul

added theorem ConcaveOn.sub

added theorem ConcaveOn.sub_strictConvexOn

added theorem ConcaveOn.subset

added theorem ConcaveOn.translate_left

added theorem ConcaveOn.translate_right

added def ConcaveOn

added theorem ConvexOn.add

added theorem ConvexOn.add_strictConvexOn

added theorem ConvexOn.comp

added theorem ConvexOn.comp_affineMap

added theorem ConvexOn.comp_concaveOn

added theorem ConvexOn.comp_linearMap

added theorem ConvexOn.convex_epigraph

added theorem ConvexOn.convex_le

added theorem ConvexOn.convex_lt

added theorem ConvexOn.convex_strict_epigraph

added theorem ConvexOn.dual

added theorem ConvexOn.le_left_of_right_le''

added theorem ConvexOn.le_left_of_right_le'

added theorem ConvexOn.le_left_of_right_le

added theorem ConvexOn.le_on_segment'

added theorem ConvexOn.le_on_segment

added theorem ConvexOn.le_right_of_left_le''

added theorem ConvexOn.le_right_of_left_le'

added theorem ConvexOn.le_right_of_left_le

added theorem ConvexOn.lt_left_of_right_lt'

added theorem ConvexOn.lt_left_of_right_lt

added theorem ConvexOn.lt_right_of_left_lt'

added theorem ConvexOn.lt_right_of_left_lt

added theorem ConvexOn.openSegment_subset_strict_epigraph

added theorem ConvexOn.smul

added theorem ConvexOn.sub

added theorem ConvexOn.sub_strictConcaveOn

added theorem ConvexOn.subset

added theorem ConvexOn.sup

added theorem ConvexOn.translate_left

added theorem ConvexOn.translate_right

added def ConvexOn

added theorem LinearMap.concaveOn

added theorem LinearMap.convexOn

added theorem LinearOrder.concaveOn_of_lt

added theorem LinearOrder.convexOn_of_lt

added theorem LinearOrder.strictConcaveOn_of_lt

added theorem LinearOrder.strictConvexOn_of_lt

added theorem StrictConcaveOn.add

added theorem StrictConcaveOn.add_concaveOn

added theorem StrictConcaveOn.comp

added theorem StrictConcaveOn.comp_strictConvexOn

added theorem StrictConcaveOn.concaveOn

added theorem StrictConcaveOn.convex_gt

added theorem StrictConcaveOn.dual

added theorem StrictConcaveOn.inf

added theorem StrictConcaveOn.lt_on_openSegment

added theorem StrictConcaveOn.lt_on_open_segment'

added theorem StrictConcaveOn.sub

added theorem StrictConcaveOn.sub_convexOn

added theorem StrictConcaveOn.subset

added theorem StrictConcaveOn.translate_left

added theorem StrictConcaveOn.translate_right

added def StrictConcaveOn

added theorem StrictConvexOn.add

added theorem StrictConvexOn.add_convexOn

added theorem StrictConvexOn.comp

added theorem StrictConvexOn.comp_strictConcaveOn

added theorem StrictConvexOn.convexOn

added theorem StrictConvexOn.convex_lt

added theorem StrictConvexOn.dual

added theorem StrictConvexOn.lt_on_openSegment

added theorem StrictConvexOn.lt_on_open_segment'

added theorem StrictConvexOn.sub

added theorem StrictConvexOn.sub_concaveOn

added theorem StrictConvexOn.subset

added theorem StrictConvexOn.sup

added theorem StrictConvexOn.translate_left

added theorem StrictConvexOn.translate_right

added def StrictConvexOn

added theorem concaveOn_const

added theorem concaveOn_id

added theorem concaveOn_iff_convex_hypograph

added theorem concaveOn_iff_div

added theorem concaveOn_iff_forall_pos

added theorem concaveOn_iff_pairwise_pos

added theorem concaveOn_of_convex_hypograph

added theorem convexOn_const

added theorem convexOn_id

added theorem convexOn_iff_convex_epigraph

added theorem convexOn_iff_div

added theorem convexOn_iff_forall_pos

added theorem convexOn_iff_pairwise_pos

added theorem convexOn_of_convex_epigraph

added theorem neg_concaveOn_iff

added theorem neg_convexOn_iff

added theorem neg_strictConcaveOn_iff

added theorem neg_strictConvexOn_iff

added theorem strictConcaveOn_iff_div

added theorem strictConvexOn_iff_div