Commit 2023-09-08 11:01 5959edf8

View on Github →

feat: cleanup API around differentiable functions (#7004) First calculus prerequisites for Rademacher theorem in #7003. Add a few lemmas that were available for FDeriv but not for Deriv, weaken assumptions here and there.

Estimated changes

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

added theorem Filter.EventuallyEq.hasDerivAt_iff

added theorem Filter.EventuallyEq.hasDerivWithinAt_iff

added theorem Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem

added theorem HasDerivAt.le_of_lip'

added theorem HasDerivAt.le_of_lipschitz

added theorem HasDerivAt.le_of_lipschitzOn

added theorem derivWithin_of_mem_nhds

modified theorem derivWithin_of_open

added theorem norm_derivWithin_eq_norm_fderivWithin

added theorem norm_deriv_eq_norm_fderiv

added theorem norm_deriv_le_of_lip'

added theorem norm_deriv_le_of_lipschitz

added theorem norm_deriv_le_of_lipschitzOn

Modified Mathlib/Analysis/Calculus/Deriv/Slope.lean

added theorem HasDerivAt.tendsto_slope_zero_left

added theorem HasDerivAt.tendsto_slope_zero_right

added theorem hasDerivAt_iff_tendsto_slope_zero

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

deleted theorem DifferentiableAt.le_of_lip

deleted theorem HasFDerivAt.le_of_lip

added theorem HasFDerivAt.le_of_lipschitz

added theorem HasFDerivAt.le_of_lipschitzOn

added theorem norm_fderiv_le_of_lip'

added theorem norm_fderiv_le_of_lipschitz

added theorem norm_fderiv_le_of_lipschitzOn

Modified Mathlib/Analysis/Calculus/MeanValue.lean

modified theorem eq_of_fderiv_eq

modified theorem is_const_of_fderiv_eq_zero

added theorem lipschitzWith_of_nnnorm_fderiv_le