Commit 2025-04-19 14:42 06feae04

View on Github →

refactor(Calculus/MeanValue): move some theorems to Deriv/ (#24190)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Deriv/MeanValue.lean

added theorem Convex.image_sub_le_mul_sub_of_deriv_le

added theorem Convex.image_sub_lt_mul_sub_of_deriv_lt

added theorem Convex.mul_sub_le_image_sub_of_le_deriv

added theorem Convex.mul_sub_lt_image_sub_of_lt_deriv

added theorem antitoneOn_of_deriv_nonpos

added theorem antitoneOn_of_hasDerivWithinAt_nonpos

added theorem antitone_of_deriv_nonpos

added theorem antitone_of_hasDerivAt_nonpos

added theorem domain_mvt

added theorem exists_deriv_eq_slope'

added theorem exists_deriv_eq_slope

added theorem exists_hasDerivAt_eq_slope

added theorem exists_ratio_deriv_eq_ratio_slope'

added theorem exists_ratio_deriv_eq_ratio_slope

added theorem exists_ratio_hasDerivAt_eq_ratio_slope'

added theorem exists_ratio_hasDerivAt_eq_ratio_slope

added theorem image_sub_le_mul_sub_of_deriv_le

added theorem image_sub_lt_mul_sub_of_deriv_lt

added theorem monotoneOn_of_deriv_nonneg

added theorem monotoneOn_of_hasDerivWithinAt_nonneg

added theorem monotone_of_deriv_nonneg

added theorem monotone_of_hasDerivAt_nonneg

added theorem mul_sub_le_image_sub_of_le_deriv

added theorem mul_sub_lt_image_sub_of_lt_deriv

added theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio

added theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi

added theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio

added theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi

added theorem strictAntiOn_of_deriv_neg

added theorem strictAntiOn_of_hasDerivWithinAt_neg

added theorem strictAnti_of_deriv_neg

added theorem strictAnti_of_hasDerivAt_neg

added theorem strictMonoOn_of_deriv_pos

added theorem strictMonoOn_of_hasDerivWithinAt_pos

added theorem strictMono_of_deriv_pos

added theorem strictMono_of_hasDerivAt_pos

Modified Mathlib/Analysis/Calculus/FirstDerivativeTest.lean

Modified Mathlib/Analysis/Calculus/LHopital.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

deleted theorem Convex.image_sub_le_mul_sub_of_deriv_le

deleted theorem Convex.image_sub_lt_mul_sub_of_deriv_lt

deleted theorem Convex.mul_sub_le_image_sub_of_le_deriv

deleted theorem Convex.mul_sub_lt_image_sub_of_lt_deriv

deleted theorem antitoneOn_of_deriv_nonpos

deleted theorem antitoneOn_of_hasDerivWithinAt_nonpos

deleted theorem antitone_of_deriv_nonpos

deleted theorem antitone_of_hasDerivAt_nonpos

deleted theorem domain_mvt

deleted theorem exists_deriv_eq_slope'

deleted theorem exists_deriv_eq_slope

deleted theorem exists_hasDerivAt_eq_slope

deleted theorem exists_ratio_deriv_eq_ratio_slope'

deleted theorem exists_ratio_deriv_eq_ratio_slope

deleted theorem exists_ratio_hasDerivAt_eq_ratio_slope'

deleted theorem exists_ratio_hasDerivAt_eq_ratio_slope

deleted theorem image_sub_le_mul_sub_of_deriv_le

deleted theorem image_sub_lt_mul_sub_of_deriv_lt

deleted theorem monotoneOn_of_deriv_nonneg

deleted theorem monotoneOn_of_hasDerivWithinAt_nonneg

deleted theorem monotone_of_deriv_nonneg

deleted theorem monotone_of_hasDerivAt_nonneg

deleted theorem mul_sub_le_image_sub_of_le_deriv

deleted theorem mul_sub_lt_image_sub_of_lt_deriv

deleted theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Iio

deleted theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi

deleted theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio

deleted theorem not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi

deleted theorem strictAntiOn_of_deriv_neg

deleted theorem strictAntiOn_of_hasDerivWithinAt_neg

deleted theorem strictAnti_of_deriv_neg

deleted theorem strictAnti_of_hasDerivAt_neg

deleted theorem strictMonoOn_of_deriv_pos

deleted theorem strictMonoOn_of_hasDerivWithinAt_pos

deleted theorem strictMono_of_deriv_pos

deleted theorem strictMono_of_hasDerivAt_pos

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/Convex/Deriv.lean

Modified Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean