Commit 2023-05-21 21:51 2a3dcf0c

View on Github →

feat: port Analysis.Calculus.FDeriv.Basic (#4132)

Estimated changes

Modified Mathlib.lean

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

added theorem Asymptotics.IsBigO.hasFDerivAt

added theorem Asymptotics.IsBigO.hasFDerivWithinAt

added theorem Differentiable.continuous

added theorem Differentiable.differentiableAt

added theorem Differentiable.differentiableOn

added def Differentiable

added theorem DifferentiableAt.congr_of_eventuallyEq

added theorem DifferentiableAt.continuousAt

added theorem DifferentiableAt.differentiableWithinAt

added theorem DifferentiableAt.fderivWithin

added theorem DifferentiableAt.hasFDerivAt

added theorem DifferentiableAt.le_of_lip

added def DifferentiableAt

added theorem DifferentiableOn.congr

added theorem DifferentiableOn.congr_mono

added theorem DifferentiableOn.continuousOn

added theorem DifferentiableOn.differentiableAt

added theorem DifferentiableOn.eventually_differentiableAt

added theorem DifferentiableOn.hasFDerivAt

added theorem DifferentiableOn.mono

added def DifferentiableOn

added theorem DifferentiableWithinAt.antimono

added theorem DifferentiableWithinAt.congr

added theorem DifferentiableWithinAt.congr_mono

added theorem DifferentiableWithinAt.congr_of_eventuallyEq

added theorem DifferentiableWithinAt.continuousWithinAt

added theorem DifferentiableWithinAt.differentiableAt

added theorem DifferentiableWithinAt.fderivWithin_congr_mono

added theorem DifferentiableWithinAt.hasFDerivWithinAt

added theorem DifferentiableWithinAt.mono

added theorem DifferentiableWithinAt.mono_of_mem

added def DifferentiableWithinAt

added theorem Filter.EventuallyEq.differentiableAt_iff

added theorem Filter.EventuallyEq.differentiableWithinAt_iff

added theorem Filter.EventuallyEq.differentiableWithinAt_iff_of_mem

added theorem Filter.EventuallyEq.fderivWithin_eq

added theorem Filter.EventuallyEq.fderivWithin_eq_nhds

added theorem Filter.EventuallyEq.fderiv_eq

added theorem Filter.EventuallyEq.hasFDerivAtFilter_iff

added theorem Filter.EventuallyEq.hasFDerivAt_iff

added theorem Filter.EventuallyEq.hasFDerivWithinAt_iff

added theorem Filter.EventuallyEq.hasFDerivWithinAt_iff_of_mem

added theorem Filter.EventuallyEq.hasStrictFDerivAt_iff

added theorem HasCompactSupport.fderiv

added theorem HasFDerivAt.congr_of_eventuallyEq

added theorem HasFDerivAt.continuousAt

added theorem HasFDerivAt.differentiableAt

added theorem HasFDerivAt.fderiv

added theorem HasFDerivAt.hasFDerivAtFilter

added theorem HasFDerivAt.hasFDerivWithinAt

added theorem HasFDerivAt.le_of_lip'

added theorem HasFDerivAt.le_of_lip

added theorem HasFDerivAt.lim

added theorem HasFDerivAt.unique

added def HasFDerivAt

added theorem HasFDerivAtFilter.congr_of_eventuallyEq

added theorem HasFDerivAtFilter.isBigO_sub

added theorem HasFDerivAtFilter.isBigO_sub_rev

added theorem HasFDerivAtFilter.tendsto_nhds

added def HasFDerivAtFilter

added theorem HasFDerivWithinAt.antimono

added theorem HasFDerivWithinAt.congr'

added theorem HasFDerivWithinAt.congr

added theorem HasFDerivWithinAt.congr_mono

added theorem HasFDerivWithinAt.congr_of_eventuallyEq

added theorem HasFDerivWithinAt.continuousWithinAt

added theorem HasFDerivWithinAt.differentiableWithinAt

added theorem HasFDerivWithinAt.fderivWithin

added theorem HasFDerivWithinAt.hasFDerivAt

added theorem HasFDerivWithinAt.insert

added theorem HasFDerivWithinAt.lim

added theorem HasFDerivWithinAt.mono_of_mem

added theorem HasFDerivWithinAt.nhdsWithin

added theorem HasFDerivWithinAt.union

added theorem HasFDerivWithinAt.unique_on

added def HasFDerivWithinAt

added theorem HasStrictFDerivAt.congr_of_eventuallyEq

added theorem HasStrictFDerivAt.exists_lipschitzOnWith

added theorem HasStrictFDerivAt.exists_lipschitzOnWith_of_nnnorm_lt

added theorem HasStrictFDerivAt.isBigO_sub

added theorem HasStrictFDerivAt.isBigO_sub_rev

added def HasStrictFDerivAt

added theorem Set.Subsingleton.differentiableOn

added theorem UniqueDiffOn.eq

added theorem UniqueDiffWithinAt.eq

added theorem differentiableAt_const

added theorem differentiableAt_id'

added theorem differentiableAt_id

added theorem differentiableOn_congr

added theorem differentiableOn_const

added theorem differentiableOn_empty

added theorem differentiableOn_id

added theorem differentiableOn_of_locally_differentiableOn

added theorem differentiableOn_singleton

added theorem differentiableOn_univ

added theorem differentiableWithinAt_const

added theorem differentiableWithinAt_id

added theorem differentiableWithinAt_inter'

added theorem differentiableWithinAt_inter

added theorem differentiableWithinAt_univ

added theorem differentiable_const

added theorem differentiable_id'

added theorem differentiable_id

added def fderiv

added def fderivWithin

added theorem fderivWithin_congr'

added theorem fderivWithin_congr

added theorem fderivWithin_const_apply

added theorem fderivWithin_eq_fderiv

added theorem fderivWithin_id'

added theorem fderivWithin_id

added theorem fderivWithin_inter

added theorem fderivWithin_mem_iff

added theorem fderivWithin_of_mem_nhds

added theorem fderivWithin_of_open

added theorem fderivWithin_subset'

added theorem fderivWithin_subset

added theorem fderivWithin_univ

added theorem fderivWithin_zero_of_not_differentiableWithinAt

added theorem fderiv_const

added theorem fderiv_const_apply

added theorem fderiv_eq

added theorem fderiv_id'

added theorem fderiv_id

added theorem fderiv_mem_iff

added theorem fderiv_zero_of_not_differentiableAt

added theorem hasFDerivAtFilter_const

added theorem hasFDerivAtFilter_id

added theorem hasFDerivAtFilter_iff_tendsto

added theorem hasFDerivAt_const

added theorem hasFDerivAt_id

added theorem hasFDerivAt_iff_isLittleO_nhds_zero

added theorem hasFDerivAt_iff_tendsto

added theorem hasFDerivAt_of_subsingleton

added theorem hasFDerivAt_zero_of_eventually_const

added theorem hasFDerivWithinAt_const

added theorem hasFDerivWithinAt_id

added theorem hasFDerivWithinAt_iff_tendsto

added theorem hasFDerivWithinAt_insert

added theorem hasFDerivWithinAt_inter'

added theorem hasFDerivWithinAt_inter

added theorem hasFDerivWithinAt_of_not_mem_closure

added theorem hasFDerivWithinAt_singleton

added theorem hasFDerivWithinAt_univ

added theorem hasStrictFDerivAt_const

added theorem hasStrictFDerivAt_id

added theorem support_fderiv_subset