Commit 2023-05-29 19:05 3318c2d2

View on Github →

feat: port Analysis.Calculus.LocalExtr (#4247)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/LocalExtr.lean

added theorem IsLocalExtr.deriv_eq_zero

added theorem IsLocalExtr.fderiv_eq_zero

added theorem IsLocalExtr.hasDerivAt_eq_zero

added theorem IsLocalExtr.hasFDerivAt_eq_zero

added theorem IsLocalMax.deriv_eq_zero

added theorem IsLocalMax.fderiv_eq_zero

added theorem IsLocalMax.hasDerivAt_eq_zero

added theorem IsLocalMax.hasFDerivAt_eq_zero

added theorem IsLocalMaxOn.fderivWithin_eq_zero

added theorem IsLocalMaxOn.fderivWithin_nonpos

added theorem IsLocalMaxOn.hasFDerivWithinAt_eq_zero

added theorem IsLocalMaxOn.hasFDerivWithinAt_nonpos

added theorem IsLocalMin.deriv_eq_zero

added theorem IsLocalMin.fderiv_eq_zero

added theorem IsLocalMin.hasDerivAt_eq_zero

added theorem IsLocalMin.hasFDerivAt_eq_zero

added theorem IsLocalMinOn.fderivWithin_eq_zero

added theorem IsLocalMinOn.fderivWithin_nonneg

added theorem IsLocalMinOn.hasFDerivWithinAt_eq_zero

added theorem IsLocalMinOn.hasFDerivWithinAt_nonneg

added theorem Polynomial.card_rootSet_le_derivative

added theorem Polynomial.card_roots_le_derivative

added theorem Polynomial.card_roots_toFinset_le_card_roots_derivative_diff_roots_succ

added theorem Polynomial.card_roots_toFinset_le_derivative

added theorem exists_Ioo_extr_on_Icc

added theorem exists_deriv_eq_zero'

added theorem exists_deriv_eq_zero

added theorem exists_hasDerivAt_eq_zero'

added theorem exists_hasDerivAt_eq_zero

added theorem exists_local_extr_Ioo

added theorem mem_posTangentConeAt_of_segment_subset'

added theorem mem_posTangentConeAt_of_segment_subset

added def posTangentConeAt

added theorem posTangentConeAt_mono

added theorem posTangentConeAt_univ