Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-06 13:44 850d5d28

View on Github →

feat(analysis/convex/function): Dual lemmas (#9571)

Estimated changes

Modified src/analysis/convex/function.lean

added theorem concave_on.convex_gt

deleted theorem concave_on.convex_lt

added theorem concave_on.dual

added theorem concave_on.ge_on_segment'

added theorem concave_on.ge_on_segment

deleted theorem concave_on.le_on_segment'

deleted theorem concave_on.le_on_segment

modified theorem concave_on.smul

added theorem convex_on.dual

modified theorem convex_on.smul

added theorem strict_concave_on.dual

added theorem strict_convex_on.dual