Commit 2023-05-28 04:44 410924a5

View on Github →

feat: port Analysis.Calculus.Deriv.Basic (#4434)

Estimated changes

Modified Mathlib.lean

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

added theorem DifferentiableAt.derivWithin

added theorem DifferentiableAt.hasDerivAt

added theorem DifferentiableOn.hasDerivAt

added theorem DifferentiableWithinAt.hasDerivWithinAt

added theorem Filter.EventuallyEq.derivWithin_eq

added theorem Filter.EventuallyEq.deriv_eq

added theorem Filter.EventuallyEq.hasDerivAtFilter_iff

added theorem HasDerivAt.congr_of_eventuallyEq

added theorem HasDerivAt.continuousAt

added theorem HasDerivAt.deriv

added theorem HasDerivAt.differentiableAt

added theorem HasDerivAt.hasDerivAtFilter

added theorem HasDerivAt.hasDerivWithinAt

added theorem HasDerivAt.unique

added def HasDerivAt

added theorem HasDerivAtFilter.congr_of_eventuallyEq

added theorem HasDerivAtFilter.isBigO_sub

added theorem HasDerivAtFilter.mono

added def HasDerivAtFilter

added theorem HasDerivWithinAt.Ioi_iff_Ioo

added theorem HasDerivWithinAt.congr

added theorem HasDerivWithinAt.congr_mono

added theorem HasDerivWithinAt.congr_of_eventuallyEq

added theorem HasDerivWithinAt.congr_of_eventuallyEq_of_mem

added theorem HasDerivWithinAt.congr_of_mem

added theorem HasDerivWithinAt.continuousWithinAt

added theorem HasDerivWithinAt.derivWithin

added theorem HasDerivWithinAt.deriv_eq_zero

added theorem HasDerivWithinAt.differentiableWithinAt

added theorem HasDerivWithinAt.hasDerivAt

added theorem HasDerivWithinAt.hasFDerivWithinAt

added theorem HasDerivWithinAt.mono

added theorem HasDerivWithinAt.mono_of_mem

added theorem HasDerivWithinAt.nhdsWithin

added theorem HasDerivWithinAt.union

added def HasDerivWithinAt

added theorem HasFDerivAt.hasDerivAt

added theorem HasFDerivAtFilter.hasDerivAtFilter

added theorem HasFDerivWithinAt.hasDerivWithinAt

added theorem HasStrictDerivAt.hasDerivAt

added def HasStrictDerivAt

added theorem UniqueDiffWithinAt.eq_deriv

added def deriv

added def derivWithin

added theorem derivWithin_Ioi_eq_Ici

added theorem derivWithin_congr

added theorem derivWithin_congr_set'

added theorem derivWithin_congr_set

added theorem derivWithin_const

added theorem derivWithin_fderivWithin

added theorem derivWithin_id

added theorem derivWithin_inter

added theorem derivWithin_mem_iff

added theorem derivWithin_of_mem

added theorem derivWithin_of_open

added theorem derivWithin_subset

added theorem derivWithin_univ

added theorem derivWithin_zero_of_not_differentiableWithinAt

added theorem deriv_const'

added theorem deriv_const

added theorem deriv_eq

added theorem deriv_fderiv

added theorem deriv_id''

added theorem deriv_id'

added theorem deriv_id

added theorem deriv_mem_iff

added theorem deriv_zero_of_not_differentiableAt

added theorem differentiableAt_of_deriv_ne_zero

added theorem differentiableWithinAt_Ioi_iff_Ici

added theorem differentiableWithinAt_of_derivWithin_ne_zero

added theorem fderivWithin_derivWithin

added theorem fderiv_deriv

added theorem hasDerivAtFilter_const

added theorem hasDerivAtFilter_id

added theorem hasDerivAtFilter_iff_isLittleO

added theorem hasDerivAtFilter_iff_tendsto

added theorem hasDerivAt_const

added theorem hasDerivAt_deriv_iff

added theorem hasDerivAt_id'

added theorem hasDerivAt_id

added theorem hasDerivAt_iff_hasFDerivAt

added theorem hasDerivAt_iff_isLittleO

added theorem hasDerivAt_iff_isLittleO_nhds_zero

added theorem hasDerivAt_iff_tendsto

added theorem hasDerivWithinAt_Iio_iff_Iic

added theorem hasDerivWithinAt_Ioi_iff_Ici

added theorem hasDerivWithinAt_congr_set'

added theorem hasDerivWithinAt_congr_set

added theorem hasDerivWithinAt_const

added theorem hasDerivWithinAt_derivWithin_iff

added theorem hasDerivWithinAt_diff_singleton

added theorem hasDerivWithinAt_id

added theorem hasDerivWithinAt_iff_hasFDerivWithinAt

added theorem hasDerivWithinAt_iff_isLittleO

added theorem hasDerivWithinAt_iff_tendsto

added theorem hasDerivWithinAt_inter'

added theorem hasDerivWithinAt_inter

added theorem hasDerivWithinAt_univ

added theorem hasFDerivAtFilter_iff_hasDerivAtFilter

added theorem hasFDerivAt_iff_hasDerivAt

added theorem hasFDerivWithinAt_iff_hasDerivWithinAt

added theorem hasStrictDerivAt_const

added theorem hasStrictDerivAt_id

added theorem hasStrictDerivAt_iff_hasStrictFDerivAt

added theorem hasStrictFDerivAt_iff_hasStrictDerivAt