Commit 2026-04-03 21:39 52c287b1

View on Github →

feat: add more APIs for the first derivative test (#34717) The derivative test in Mathlib right now only says whether a point is local maximum. This is hard to use in practice (for example in the PNT project) as we sometimes want to show that a point is a maximum on some interval. This PR adds more APIs for the first derivative test to resolve this issue.

Estimated changes

modified theorem isLocalMin_of_deriv_Ioo
added theorem isMaxOn_Icc_of_deriv
added theorem isMaxOn_Ici_of_deriv
added theorem isMaxOn_Ico_of_deriv
added theorem isMaxOn_Iic_of_deriv
added theorem isMaxOn_Iio_of_deriv
added theorem isMaxOn_Ioc_of_deriv
added theorem isMaxOn_Ioi_of_deriv
added theorem isMaxOn_Ioo_of_deriv
added theorem isMaxOn_univ_of_deriv
added theorem isMinOn_Icc_of_deriv
added theorem isMinOn_Ici_of_deriv
added theorem isMinOn_Ico_of_deriv
added theorem isMinOn_Iic_of_deriv
added theorem isMinOn_Iio_of_deriv
added theorem isMinOn_Ioc_of_deriv
added theorem isMinOn_Ioi_of_deriv
added theorem isMinOn_Ioo_of_deriv
added theorem isMinOn_univ_of_deriv