Commit 2023-05-25 03:53 1b43f3b7

View on Github →

feat: port Analysis.Convex.SpecificFunctions.Basic (#4142)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/SpecificFunctions/Basic.lean

added theorem convexOn_exp

added theorem convexOn_pow

added theorem convexOn_rpow

added theorem convexOn_zpow

added theorem one_add_mul_self_le_rpow_one_add

added theorem one_add_mul_self_lt_rpow_one_add

added theorem strictConcaveOn_log_Iio

added theorem strictConcaveOn_log_Ioi

added theorem strictConvexOn_exp

added theorem strictConvexOn_rpow