Commit 2021-11-08 16:03 66dea297

View on Github →

feat(analysis/convex/specific_functions): Strict convexity of exp, log and pow (#10123) This strictifies the results of convexity/concavity of exp/log and add the strict versions for pow, zpow, rpow. I'm also renaming convex_on_pow_of_even to even.convex_on_pow for dot notation.

Estimated changes

Modified src/analysis/convex/specific_functions.lean

deleted theorem concave_on_log_Iio

deleted theorem concave_on_log_Ioi

modified theorem convex_on_exp

deleted theorem convex_on_pow_of_even

added theorem even.convex_on_pow

added theorem even.strict_convex_on_pow

added theorem int_prod_range_pos

added theorem strict_concave_on_log_Iio

added theorem strict_concave_on_log_Ioi

added theorem strict_convex_on_exp

added theorem strict_convex_on_pow

added theorem strict_convex_on_rpow

added theorem strict_convex_on_zpow

Modified src/analysis/mean_inequalities.lean