Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-17 15:28 d4cb2372

View on Github →

feat(algebra/module): define ordered semimodules and generalize convexity of functions (#3728)

Estimated changes

Created src/algebra/module/ordered.lean

added theorem smul_le_smul_of_nonneg

added theorem smul_lt_smul_of_pos

Modified src/analysis/convex/basic.lean

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.le_on_segment'

modified theorem convex_on.le_on_segment

modified theorem convex_on.smul

modified theorem convex_on.subset

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_iff_convex_epigraph

deleted theorem convex_on_iff_div:

added theorem convex_on_iff_div

modified theorem linear_order.convex_on_of_lt

Modified src/analysis/convex/specific_functions.lean

modified theorem convex_on_fpow

modified theorem convex_on_pow

modified theorem convex_on_pow_of_even

modified theorem convex_on_rpow