Additive operations on derivatives #
For detailed documentation of the FrΓ©chet derivative,
see the module docstring of Analysis/Calculus/FDeriv/Basic.lean
.
This file contains the usual formulas (and existence assertions) for the derivative of
- sum of finitely many functions
- multiplication of a function by a scalar constant
- negative of a function
- subtraction of two functions
Derivative of a function multiplied by a constant #
Alias of fderivWithin_const_smul
.
Alias of fderiv_const_smul
.
Derivative of the sum of two functions #
Alias of fderivWithin_add
.
Alias of fderiv_add
.
Alias of the reverse direction of hasFDerivAtFilter_add_const_iff
.
Alias of the reverse direction of hasStrictFDerivAt_add_const_iff
.
Alias of the reverse direction of hasFDerivWithinAt_add_const_iff
.
Alias of the reverse direction of hasFDerivAt_add_const_iff
.
Alias of the reverse direction of differentiableWithinAt_add_const_iff
.
Alias of the reverse direction of differentiableAt_add_const_iff
.
Alias of the reverse direction of differentiableOn_add_const_iff
.
Alias of the reverse direction of differentiable_add_const_iff
.
Alias of the reverse direction of hasFDerivAtFilter_const_add_iff
.
Alias of the reverse direction of hasStrictFDerivAt_const_add_iff
.
Alias of the reverse direction of hasFDerivWithinAt_const_add_iff
.
Alias of the reverse direction of hasFDerivAt_const_add_iff
.
Alias of the reverse direction of differentiableWithinAt_const_add_iff
.
Alias of the reverse direction of differentiableAt_const_add_iff
.
Alias of the reverse direction of differentiableOn_const_add_iff
.
Alias of the reverse direction of differentiable_const_add_iff
.
Derivative of a finite sum of functions #
Derivative of the negative of a function #
Alias of fderivWithin_neg
.
Version of fderiv_neg
where the function is written -f
instead of fun y β¦ - f y
.
Alias of fderiv_neg
.
Version of fderiv_neg
where the function is written -f
instead of fun y β¦ - f y
.
Derivative of the difference of two functions #
Alias of fderivWithin_sub
.
Alias of fderiv_sub
.
Alias of the reverse direction of hasFDerivAtFilter_sub_const_iff
.
Alias of the reverse direction of hasStrictFDerivAt_sub_const_iff
.
Alias of the reverse direction of hasFDerivWithinAt_sub_const_iff
.
Alias of the reverse direction of hasFDerivAt_sub_const_iff
.