Mathlib Changelog
v3
Changelog
About
Github
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