Commit 2021-09-17 14:39 dfd4bf5d

View on Github →

split(analysis/convex/function): move convex_on and concave_on to their own file (#9247) Convex/concave functions now earn their own file. This cuts down analysis.convex.basic by 500 lines.

Estimated changes

Modified src/analysis/convex/basic.lean

deleted theorem concave_on.add

deleted theorem concave_on.comp_affine_map

deleted theorem concave_on.comp_linear_map

deleted theorem concave_on.concave_le

deleted theorem concave_on.convex_hypograph

deleted theorem concave_on.convex_lt

deleted theorem concave_on.inf

deleted theorem concave_on.le_on_segment'

deleted theorem concave_on.le_on_segment

deleted theorem concave_on.le_right_of_left_le'

deleted theorem concave_on.le_right_of_left_le

deleted theorem concave_on.left_le_of_le_right'

deleted theorem concave_on.left_le_of_le_right

deleted theorem concave_on.slope_mono_adjacent

deleted theorem concave_on.smul

deleted theorem concave_on.subset

deleted theorem concave_on.translate_left

deleted theorem concave_on.translate_right

deleted def concave_on

deleted theorem concave_on_const

deleted theorem concave_on_id

deleted theorem concave_on_iff_convex_hypograph

deleted theorem concave_on_iff_div

deleted theorem concave_on_real_iff_slope_mono_adjacent

deleted theorem concave_on_real_of_slope_mono_adjacent

deleted theorem convex_on.add

deleted theorem convex_on.comp_affine_map

deleted theorem convex_on.comp_linear_map

deleted theorem convex_on.convex_epigraph

deleted theorem convex_on.convex_le

deleted theorem convex_on.convex_lt

deleted theorem convex_on.le_left_of_right_le'

deleted theorem convex_on.le_left_of_right_le

deleted theorem convex_on.le_on_segment'

deleted theorem convex_on.le_on_segment

deleted theorem convex_on.le_right_of_left_le'

deleted theorem convex_on.le_right_of_left_le

deleted theorem convex_on.slope_mono_adjacent

deleted theorem convex_on.smul

deleted theorem convex_on.subset

deleted theorem convex_on.sup

deleted theorem convex_on.translate_left

deleted theorem convex_on.translate_right

deleted def convex_on

deleted theorem convex_on_const

deleted theorem convex_on_id

deleted theorem convex_on_iff_convex_epigraph

deleted theorem convex_on_iff_div

deleted theorem convex_on_real_iff_slope_mono_adjacent

deleted theorem convex_on_real_of_slope_mono_adjacent

deleted theorem linear_map.concave_on

deleted theorem linear_map.convex_on

deleted theorem linear_order.concave_on_of_lt

deleted theorem linear_order.convex_on_of_lt

deleted theorem neg_concave_on_iff

deleted theorem neg_convex_on_iff

Modified src/analysis/convex/combination.lean

deleted theorem convex_on.exists_ge_of_center_mass

deleted theorem convex_on.exists_ge_of_mem_convex_hull

deleted theorem convex_on.map_center_mass_le

deleted theorem convex_on.map_sum_le

Modified src/analysis/convex/exposed.lean

Modified src/analysis/convex/extrema.lean

Created src/analysis/convex/function.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.inf

added theorem concave_on.le_on_segment'

added theorem concave_on.le_on_segment

added theorem concave_on.le_right_of_left_le'

added theorem concave_on.le_right_of_left_le

added theorem concave_on.left_le_of_le_right'

added theorem concave_on.left_le_of_le_right

added theorem concave_on.slope_mono_adjacent

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_iff_slope_mono_adjacent

added theorem concave_on_real_of_slope_mono_adjacent

added theorem convex_on.add

added theorem convex_on.comp_affine_map

added theorem convex_on.comp_linear_map

added theorem convex_on.convex_epigraph

added theorem convex_on.convex_le

added theorem convex_on.convex_lt

added theorem convex_on.exists_ge_of_center_mass

added theorem convex_on.exists_ge_of_mem_convex_hull

added theorem convex_on.le_left_of_right_le'

added theorem convex_on.le_left_of_right_le

added theorem convex_on.le_on_segment'

added theorem convex_on.le_on_segment

added theorem convex_on.le_right_of_left_le'

added theorem convex_on.le_right_of_left_le

added theorem convex_on.map_center_mass_le

added theorem convex_on.map_sum_le

added theorem convex_on.slope_mono_adjacent

added theorem convex_on.smul

added theorem convex_on.subset

added theorem convex_on.sup

added theorem convex_on.translate_left

added theorem convex_on.translate_right

added def convex_on

added theorem convex_on_const

added theorem convex_on_id

added theorem convex_on_iff_convex_epigraph

added theorem convex_on_iff_div

added theorem convex_on_real_iff_slope_mono_adjacent

added theorem convex_on_real_of_slope_mono_adjacent

added theorem linear_map.concave_on

added theorem linear_map.convex_on

added theorem linear_order.concave_on_of_lt

added theorem linear_order.convex_on_of_lt

added theorem neg_concave_on_iff

added theorem neg_convex_on_iff

Modified src/analysis/convex/integral.lean

Modified src/analysis/convex/topology.lean

Modified src/linear_algebra/affine_space/ordered.lean