Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-26 07:23 def1c02a

View on Github →

refactor(analysis/convex/function): generalize definition of convex_on/concave_on to allow any (ordered) scalars (#9389) convex_on and concave_on are currently only defined for real vector spaces. This generalizes ℝ to an arbitrary ordered_semiring in the definition.

Estimated changes

modified def convex
modified theorem concave_on.add
modified theorem concave_on.comp_linear_map
modified theorem concave_on.concave_le
modified theorem concave_on.inf
modified theorem concave_on.le_on_segment'
modified theorem concave_on.le_on_segment
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 convex_on.add
modified theorem convex_on.comp_linear_map
modified theorem convex_on.convex_le
modified theorem convex_on.le_on_segment'
modified theorem convex_on.le_on_segment
modified theorem convex_on.map_sum_le
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 linear_map.concave_on
modified theorem linear_map.convex_on
modified theorem concave_on_log_Iio
modified theorem concave_on_log_Ioi
modified theorem convex_on_exp
modified theorem convex_on_fpow
modified theorem convex_on_pow
modified theorem convex_on_pow_of_even
modified theorem convex_on_rpow