Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-22 18:09 abe44595

View on Github →

feat(analysis/convex): define concavity of functions (#3849)

Estimated changes

Modified src/algebra/module/ordered.lean

Modified src/algebra/ordered_group.lean

Modified src/analysis/convex/basic.lean

added theorem concave_on.add

added theorem concave_on.comp_affine_map

added theorem concave_on.comp_linear_map

added theorem concave_on.concave_le

added theorem concave_on.convex_hypograph

added theorem concave_on.convex_lt

added theorem concave_on.le_on_segment'

added theorem concave_on.le_on_segment

added theorem concave_on.smul

added theorem concave_on.subset

added theorem concave_on.translate_left

added theorem concave_on.translate_right

added def concave_on

added theorem concave_on_const

added theorem concave_on_id

added theorem concave_on_iff_convex_hypograph

added theorem concave_on_iff_div

added theorem concave_on_real_of_slope_mono_adjacent

modified theorem convex_on.le_on_segment'

modified theorem convex_on.le_on_segment

added theorem linear_order.concave_on_of_lt

added theorem neg_concave_on_iff

added theorem neg_convex_on_iff

Modified src/analysis/convex/extrema.lean

added theorem is_max_on.of_is_local_max_of_convex_univ

added theorem is_max_on.of_is_local_max_on_of_concave_on

modified theorem is_min_on.of_is_local_min_of_convex_univ

modified theorem is_min_on.of_is_local_min_on_of_convex_on

modified theorem is_min_on.of_is_local_min_on_of_convex_on_Icc