Mathlib Changelog
v4
Changelog
About
Github
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