Commit 2025-02-14 10:09 ebe2a3f4

View on Github →

feat: left and right derivatives of a convex function (#21063) Properties of left and right derivatives of a convex function on (the interior of) a convex set: monotonicity; leftDeriv <= rightDeriv; if leftDeriv <= 0 <= rightDeriv then the function is minimal. From the TestingLowerBounds project.

Estimated changes

Modified Mathlib/Analysis/Convex/Deriv.lean

added theorem ConcaveOn.antitoneOn_slope_gt

added theorem ConcaveOn.antitoneOn_slope_lt

added theorem ConvexOn.differentiableWithinAt_Iio_of_mem_interior

added theorem ConvexOn.differentiableWithinAt_Ioi_of_mem_interior

added theorem ConvexOn.hasDerivWithinAt_leftDeriv_of_mem_interior

added theorem ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior

added theorem ConvexOn.hasDerivWithinAt_sInf_slope_of_mem_interior

added theorem ConvexOn.hasDerivWithinAt_sSup_slope_of_mem_interior

added theorem ConvexOn.isMinOn_of_leftDeriv_eq_zero

added theorem ConvexOn.isMinOn_of_leftDeriv_nonpos_of_rightDeriv_nonneg

added theorem ConvexOn.isMinOn_of_rightDeriv_eq_zero

added theorem ConvexOn.leftDeriv_eq_sSup_slope_of_mem_interior

added theorem ConvexOn.leftDeriv_le_rightDeriv_of_mem_interior

added theorem ConvexOn.monotoneOn_leftDeriv

added theorem ConvexOn.monotoneOn_rightDeriv

added theorem ConvexOn.monotoneOn_slope_gt

added theorem ConvexOn.monotoneOn_slope_lt

added theorem ConvexOn.rightDeriv_eq_sInf_slope_of_mem_interior

added theorem ConvexOn.rightDeriv_le_slope_of_mem_interior

added theorem ConvexOn.slope_le_leftDeriv_of_mem_interior

added theorem bddAbove_slope_gt_of_mem_interior

added theorem bddBelow_slope_lt_of_mem_interior

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

added theorem MonotoneOn.csInf_eq_of_subset_of_forall_exists_le

added theorem MonotoneOn.csSup_eq_of_subset_of_forall_exists_le