Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-27 17:49 9175158f

View on Github →

refactor(analysis/convex/function): generalize lemmas about convexity/concavity of functions, prove concave Jensen (#9356) convex_on and concave_on are currently only defined for real vector spaces. This generalizes ℝ to an arbitrary ordered_semiring. As a result, we now have the concave Jensen inequality for free.

Estimated changes

Modified src/analysis/calculus/mean_value.lean

Modified src/analysis/convex/basic.lean

modified theorem convex.combo_self

Modified src/analysis/convex/combination.lean

Modified src/analysis/convex/exposed.lean

Modified src/analysis/convex/function.lean

modified theorem concave_on.add

modified theorem concave_on.comp_affine_map

modified theorem concave_on.comp_linear_map

added theorem concave_on.concave_ge

deleted theorem concave_on.concave_le

modified theorem concave_on.convex_hypograph

modified theorem concave_on.convex_lt

added theorem concave_on.exists_le_of_center_mass

added theorem concave_on.exists_le_of_mem_convex_hull

modified theorem concave_on.inf

added theorem concave_on.le_map_center_mass

added theorem concave_on.le_map_sum

modified theorem concave_on.le_on_segment'

modified theorem concave_on.le_on_segment

modified theorem concave_on.le_right_of_left_le'

modified theorem concave_on.le_right_of_left_le

modified theorem concave_on.left_le_of_le_right'

modified theorem concave_on.left_le_of_le_right

modified theorem concave_on.slope_mono_adjacent

modified theorem concave_on.smul

modified theorem concave_on.subset

modified theorem concave_on.translate_left

modified theorem concave_on.translate_right

modified def concave_on

modified theorem concave_on_const

modified theorem concave_on_id

modified theorem concave_on_iff_convex_hypograph

added theorem concave_on_iff_slope_mono_adjacent

added theorem concave_on_of_slope_mono_adjacent

deleted theorem concave_on_real_iff_slope_mono_adjacent

deleted theorem concave_on_real_of_slope_mono_adjacent

modified theorem convex_on.add

modified theorem convex_on.comp_affine_map

modified theorem convex_on.comp_linear_map

modified theorem convex_on.convex_epigraph

modified theorem convex_on.convex_le

modified theorem convex_on.convex_lt

modified theorem convex_on.exists_ge_of_center_mass

modified theorem convex_on.exists_ge_of_mem_convex_hull

modified theorem convex_on.le_left_of_right_le'

modified theorem convex_on.le_left_of_right_le

modified theorem convex_on.le_on_segment'

modified theorem convex_on.le_on_segment

modified theorem convex_on.le_right_of_left_le'

modified theorem convex_on.le_right_of_left_le

modified theorem convex_on.map_center_mass_le

modified theorem convex_on.map_sum_le

modified theorem convex_on.slope_mono_adjacent

modified theorem convex_on.smul

modified theorem convex_on.subset

modified theorem convex_on.sup

modified theorem convex_on.translate_left

modified theorem convex_on.translate_right

modified def convex_on

modified theorem convex_on_const

modified theorem convex_on_id

modified theorem convex_on_iff_convex_epigraph

added theorem convex_on_iff_slope_mono_adjacent

added theorem convex_on_of_slope_mono_adjacent

deleted theorem convex_on_real_iff_slope_mono_adjacent

deleted theorem convex_on_real_of_slope_mono_adjacent

modified theorem linear_map.concave_on

modified theorem linear_map.convex_on

modified theorem linear_order.concave_on_of_lt

modified theorem linear_order.convex_on_of_lt

modified theorem neg_concave_on_iff

modified theorem neg_convex_on_iff

Modified src/analysis/convex/integral.lean