The derivative of a composition (chain rule) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
For detailed documentation of the Fréchet derivative,
see the module docstring of
This file contains the usual formulas (and existence assertions) for the derivative of
composition of functions (the chain rule).
Derivative of the composition of two functions #
For composition lemmas, we put x explicit to help the elaborator, as otherwise Lean tends to
get confused since there are too many possibilities for composition
A version of
fderiv_within.comp that is useful to rewrite the composition of two derivatives
into a single derivative. This version always applies, but creates a new side-goal
f x = y.
Ternary version of
fderiv_within.comp, with equality assumptions of basepoints added, in
order to apply more easily as a rewrite from right-to-left.
The chain rule for derivatives in the sense of strict differentiability.