Commit 2024-08-15 17:24 25706a5c

View on Github →

feat: Compute derivative of fun x ↦ f (a - x) (#15828) ... and similar. Also generalise existing lemmas to not require differentiability assumptions.

Estimated changes

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

added theorem differentiableAt_comp_add_const

added theorem differentiableAt_comp_const_add

added theorem differentiableAt_comp_const_sub

added theorem differentiableAt_comp_neg

deleted theorem differentiableAt_comp_neg_iff

added theorem differentiableAt_comp_sub_const

added theorem differentiableAt_iff_comp_add_const

added theorem differentiableAt_iff_comp_const_add

added theorem differentiableAt_iff_comp_const_sub

added theorem differentiableAt_iff_comp_neg

added theorem differentiableAt_iff_comp_sub_const

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

modified theorem HasDerivAt.comp_add_const

modified theorem HasDerivAt.comp_const_add

added theorem HasDerivAt.comp_const_sub

added theorem HasDerivAt.comp_sub_const

modified theorem deriv_comp_add_const

modified theorem deriv_comp_const_add

added theorem deriv_comp_const_sub

modified theorem deriv_comp_neg

added theorem deriv_comp_sub_const

Modified Mathlib/NumberTheory/Harmonic/GammaDeriv.lean