Commit 2021-10-08 07:32 1390b447

View on Github →

feat(analysis/convex/function): API for strict convex functions (#9437) This provides all the basic API for strict_convex_on and strict_concave_on.

Estimated changes

Modified src/analysis/convex/function.lean

deleted theorem concave_on_iff_forall_pos_ne

added theorem concave_on_iff_pairwise_on_pos

deleted theorem convex_on_iff_forall_pos_ne

added theorem convex_on_iff_pairwise_on_pos

added theorem linear_order.strict_concave_on_of_lt

added theorem linear_order.strict_convex_on_of_lt

added theorem neg_strict_concave_on_iff

added theorem neg_strict_convex_on_iff

added theorem strict_concave_on.add

added theorem strict_concave_on.concave_on

added theorem strict_concave_on.convex_gt

added theorem strict_concave_on.inf

added theorem strict_concave_on.left_lt_of_lt_right'

added theorem strict_concave_on.left_lt_of_lt_right

added theorem strict_concave_on.lt_on_open_segment'

added theorem strict_concave_on.lt_on_open_segment

added theorem strict_concave_on.lt_right_of_left_lt'

added theorem strict_concave_on.lt_right_of_left_lt

added theorem strict_concave_on.subset

added theorem strict_concave_on.translate_left

added theorem strict_concave_on.translate_right

added theorem strict_concave_on_iff_div

added theorem strict_convex_on.add

added theorem strict_convex_on.convex_lt

added theorem strict_convex_on.convex_on

added theorem strict_convex_on.lt_left_of_right_lt'

added theorem strict_convex_on.lt_left_of_right_lt

added theorem strict_convex_on.lt_on_open_segment'

added theorem strict_convex_on.lt_on_open_segment

added theorem strict_convex_on.lt_right_of_left_lt'

added theorem strict_convex_on.lt_right_of_left_lt

added theorem strict_convex_on.subset

added theorem strict_convex_on.sup

added theorem strict_convex_on.translate_left

added theorem strict_convex_on.translate_right

added theorem strict_convex_on_iff_div

Modified src/analysis/convex/slope.lean

added theorem strict_concave_on.slope_anti_adjacent

added theorem strict_concave_on_iff_slope_strict_anti_adjacent

added theorem strict_concave_on_of_slope_strict_anti_adjacent

added theorem strict_convex_on.slope_strict_mono_adjacent

added theorem strict_convex_on_iff_slope_strict_mono_adjacent

added theorem strict_convex_on_of_slope_strict_mono_adjacent