One-dimensional iterated derivatives #
This file contains a number of further results on iteratedDerivWithin
that need more imports
than are available in Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
.
Alias of iteratedDerivWithin_const_sub
.
Note: this is unrelated to iteratedDeriv_const_smul
, where the scalar multiplication works on
the domain.
Note: this is unrelated to iteratedDeriv_const_mul
, where the multiplication works on the
domain.
Note: this is unrelated to iteratedDerivWithin_const_smul
, where the scalar multiplication
works on the codomain.
Note: this is unrelated to iteratedDerivWithin_const_mul
, where the multiplication works on
the codomain.
Invariance of iterated derivatives under translation #
The iterated derivative commutes with shifting the function by a constant on the left.
The iterated derivative commutes with shifting the function by a constant on the right.