Commit 2024-04-08 14:57 372a08fe

View on Github →

feat(Analysis/Convex/Deriv): convex implies monotone deriv (#11602) The derivative of a convex function is monotone (variations on a theme)

Estimated changes

Modified Mathlib/Analysis/Convex/Deriv.lean

added theorem ConcaveOn.antitoneOn_deriv

added theorem ConcaveOn.antitoneOn_derivWithin

added theorem ConcaveOn.derivWithin_le_slope

added theorem ConcaveOn.deriv_le_slope

added theorem ConcaveOn.le_slope_of_hasDerivAt

added theorem ConcaveOn.le_slope_of_hasDerivWithinAt

added theorem ConcaveOn.le_slope_of_hasDerivWithinAt_Iio

added theorem ConcaveOn.left_deriv_le_slope

added theorem ConcaveOn.slope_le_deriv

added theorem ConcaveOn.slope_le_derivWithin

added theorem ConcaveOn.slope_le_of_hasDerivAt

added theorem ConcaveOn.slope_le_of_hasDerivWithinAt

added theorem ConcaveOn.slope_le_of_hasDerivWithinAt_Ioi

added theorem ConcaveOn.slope_le_right_deriv

added theorem ConvexOn.derivWithin_le_slope

added theorem ConvexOn.deriv_le_slope

added theorem ConvexOn.le_slope_of_hasDerivAt

added theorem ConvexOn.le_slope_of_hasDerivWithinAt

added theorem ConvexOn.le_slope_of_hasDerivWithinAt_Ioi

added theorem ConvexOn.monotoneOn_deriv

added theorem ConvexOn.monotoneOn_derivWithin

added theorem ConvexOn.right_deriv_le_slope

added theorem ConvexOn.slope_le_deriv

added theorem ConvexOn.slope_le_derivWithin

added theorem ConvexOn.slope_le_left_deriv

added theorem ConvexOn.slope_le_of_hasDerivAt

added theorem ConvexOn.slope_le_of_hasDerivWithinAt

added theorem ConvexOn.slope_le_of_hasDerivWithinAt_Iio

added theorem StrictConcaveOn.derivWithin_lt_slope

added theorem StrictConcaveOn.deriv_lt_slope

added theorem StrictConcaveOn.left_deriv_lt_slope

added theorem StrictConcaveOn.lt_slope_of_hasDerivAt

added theorem StrictConcaveOn.lt_slope_of_hasDerivWithinAt

added theorem StrictConcaveOn.lt_slope_of_hasDerivWithinAt_Iio

added theorem StrictConcaveOn.slope_lt_deriv

added theorem StrictConcaveOn.slope_lt_derivWithin

added theorem StrictConcaveOn.slope_lt_of_hasDerivAt

added theorem StrictConcaveOn.slope_lt_of_hasDerivWithinAt

added theorem StrictConcaveOn.slope_lt_of_hasDerivWithinAt_Ioi

added theorem StrictConcaveOn.slope_lt_right_deriv

added theorem StrictConcaveOn.strictAntiOn_deriv

added theorem StrictConcaveOn.strictAntiOn_derivWithin

added theorem StrictConvexOn.derivWithin_lt_slope

added theorem StrictConvexOn.deriv_lt_slope

added theorem StrictConvexOn.lt_slope_of_hasDerivAt

added theorem StrictConvexOn.lt_slope_of_hasDerivWithinAt

added theorem StrictConvexOn.lt_slope_of_hasDerivWithinAt_Ioi

added theorem StrictConvexOn.right_deriv_lt_slope

added theorem StrictConvexOn.slope_lt_deriv

added theorem StrictConvexOn.slope_lt_derivWithin

added theorem StrictConvexOn.slope_lt_left_deriv

added theorem StrictConvexOn.slope_lt_of_hasDerivAt

added theorem StrictConvexOn.slope_lt_of_hasDerivWithinAt

added theorem StrictConvexOn.slope_lt_of_hasDerivWithinAt_Iio

added theorem StrictConvexOn.strictMonoOn_deriv

added theorem StrictConvexOn.strictMonoOn_derivWithin

Modified Mathlib/LinearAlgebra/AffineSpace/Slope.lean

added theorem slope_neg

Modified Mathlib/Topology/Order/LeftRightNhds.lean

added theorem Set.OrdConnected.mem_nhdsWithin_Ici

added theorem Set.OrdConnected.mem_nhdsWithin_Iic

added theorem Set.OrdConnected.mem_nhdsWithin_Iio

added theorem Set.OrdConnected.mem_nhdsWithin_Ioi