Commit 2025-01-26 10:01 feb6a5dd

View on Github →

chore: replace right_deriv by rightDeriv in lemma names (#21076) And similarly for left_deriv. There is no leftDeriv or rightDeriv definition (they refer to a derivWithin in an interval) but they have a similar role in lemma names so should be written in the same way as definitions.

Estimated changes

Modified Mathlib/Analysis/Convex/Deriv.lean

added theorem ConcaveOn.leftDeriv_le_slope

deleted theorem ConcaveOn.left_deriv_le_slope

added theorem ConcaveOn.slope_le_rightDeriv

deleted theorem ConcaveOn.slope_le_right_deriv

added theorem ConvexOn.rightDeriv_le_slope

deleted theorem ConvexOn.right_deriv_le_slope

added theorem ConvexOn.slope_le_leftDeriv

deleted theorem ConvexOn.slope_le_left_deriv

added theorem StrictConcaveOn.leftDeriv_lt_slope

deleted theorem StrictConcaveOn.left_deriv_lt_slope

added theorem StrictConcaveOn.slope_lt_rightDeriv

deleted theorem StrictConcaveOn.slope_lt_right_deriv

added theorem StrictConvexOn.rightDeriv_lt_slope

deleted theorem StrictConvexOn.right_deriv_lt_slope

added theorem StrictConvexOn.slope_lt_leftDeriv

deleted theorem StrictConvexOn.slope_lt_left_deriv