Commit 2023-06-06 16:13 a86c4dfe

View on Github →

feat: port Analysis.Convex.SpecificFunctions.Deriv (#4738)

Estimated changes

Modified Mathlib.lean

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

added theorem Even.strictConvexOn_pow

added theorem Finset.prod_nonneg_of_card_nonpos_even

added theorem deriv2_sqrt_mul_log

added theorem deriv_sqrt_mul_log'

added theorem deriv_sqrt_mul_log

added theorem hasDerivAt_sqrt_mul_log

added theorem int_prod_range_nonneg

added theorem int_prod_range_pos

added theorem strictConcaveOn_cos_Icc

added theorem strictConcaveOn_sin_Icc

added theorem strictConcaveOn_sqrt_mul_log_Ioi

added theorem strictConvexOn_pow

added theorem strictConvexOn_zpow