Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-16 13:26 89b0cfbf

View on Github →

refactor(analysis/convex/basic): generalize convexity to vector spaces (#9058) convex and convex_hull are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semirings in definitions and abstracts it away to the correct generality in lemmas. It also generalizes the space from add_comm_group to add_comm_monoid where possible.

Estimated changes

modified theorem convex_image_has_deriv_at
modified theorem concave_on_of_deriv2_nonpos
modified theorem convex.mono_of_deriv_nonneg
modified theorem convex_on_of_deriv2_nonneg
modified theorem convex_on_of_deriv_mono
modified theorem unique_diff_on_convex
modified theorem concave_on_const
modified theorem concave_on_id
modified theorem convex.add
modified theorem convex.add_smul
modified theorem convex.add_smul_mem
modified theorem convex.add_smul_sub_mem
modified theorem convex.affine_image
modified theorem convex.affine_preimage
modified theorem convex.affinity
modified theorem convex.combo_affine_apply
added theorem convex.combo_eq_vadd
deleted theorem convex.combo_to_vadd
modified theorem convex.convex_hull_eq
modified theorem convex.inter
modified theorem convex.is_linear_image
modified theorem convex.is_linear_preimage
modified theorem convex.linear_image
modified theorem convex.linear_preimage
modified theorem convex.mem_smul_of_zero_mem
modified theorem convex.neg
modified theorem convex.neg_preimage
modified theorem convex.open_segment_subset
modified theorem convex.prod
modified theorem convex.segment_subset
modified theorem convex.smul
modified theorem convex.smul_mem_of_zero_mem
modified theorem convex.smul_preimage
modified theorem convex.sub
modified theorem convex.translate
modified theorem convex_Icc
modified theorem convex_Ici
modified theorem convex_Ico
modified theorem convex_Iic
modified theorem convex_Iio
modified theorem convex_Inter
modified theorem convex_Ioc
modified theorem convex_Ioi
modified theorem convex_Ioo
modified theorem convex_convex_hull
modified theorem convex_empty
modified theorem convex_halfspace_ge
modified theorem convex_halfspace_gt
added theorem convex_halfspace_im_ge
modified theorem convex_halfspace_im_gt
modified theorem convex_halfspace_im_le
deleted theorem convex_halfspace_im_lge
modified theorem convex_halfspace_im_lt
modified theorem convex_halfspace_le
modified theorem convex_halfspace_lt
added theorem convex_halfspace_re_ge
modified theorem convex_halfspace_re_gt
modified theorem convex_halfspace_re_le
deleted theorem convex_halfspace_re_lge
modified theorem convex_halfspace_re_lt
modified theorem convex_hull_min
modified theorem convex_hull_mono
modified theorem convex_hull_singleton
modified theorem convex_hyperplane
deleted theorem convex_iff_div:
added theorem convex_iff_div
modified theorem convex_interval
modified theorem convex_on_const
modified theorem convex_on_id
modified theorem convex_open_segment
modified theorem convex_sInter
modified theorem convex_segment
modified theorem convex_singleton
modified theorem convex_std_simplex
modified theorem convex_univ
modified theorem linear_map.concave_on
modified theorem linear_map.convex_on
modified theorem submodule.convex
modified theorem subset_convex_hull
modified theorem subspace.convex
modified theorem convex.center_mass_mem
modified theorem convex.sum_mem
modified def convex.to_cone
modified theorem convex_cone.convex
modified theorem is_extreme.convex_diff
modified theorem convex.integral_mem
modified theorem convex.closure
modified theorem convex.interior
modified theorem convex.is_path_connected
modified theorem convex_ball
modified theorem convex_closed_ball
modified theorem convex_hull_exists_dist_ge
modified theorem convex_on_dist