Commit 2021-11-02 08:23 18528404

View on Github →

feat(analysis/calculus/mean_value): Strict convexity from derivatives (#10034) This duplicates all the results relating convex/concave function and their derivatives to strictly convex/strictly concave functions.

Estimated changes

Modified src/analysis/calculus/mean_value.lean

deleted theorem antitone.concave_on_univ

added theorem antitone.concave_on_univ_of_deriv

added theorem antitone_on.concave_on_of_deriv

deleted theorem concave_on_of_deriv_antitone_on

deleted theorem convex_on_of_deriv_monotone_on

deleted theorem convex_on_univ_of_deriv_monotone

added theorem monotone.convex_on_univ_of_deriv

added theorem monotone_on.convex_on_of_deriv

added theorem strict_anti.strict_concave_on_univ_of_deriv

added theorem strict_anti_on.strict_concave_on_of_deriv

added theorem strict_concave_on_of_deriv2_neg

added theorem strict_concave_on_open_of_deriv2_neg

added theorem strict_concave_on_univ_of_deriv2_neg

added theorem strict_convex_on_of_deriv2_pos

added theorem strict_convex_on_open_of_deriv2_pos

added theorem strict_convex_on_univ_of_deriv2_pos

added theorem strict_mono.strict_convex_on_univ_of_deriv

added theorem strict_mono_on.strict_convex_on_of_deriv