# mathlib3documentation

analysis.calculus.fderiv.comp

# 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 analysis/calculus/fderiv/basic.lean.

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

theorem has_fderiv_at_filter.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {L : filter E} {g : F G} {g' : F →L[𝕜] G} {L' : filter F} (hg : (f x) L') (hf : x L) (hL : L') :
has_fderiv_at_filter (g f) (g'.comp f') x L
theorem has_fderiv_within_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} {t : set F} (hg : t (f x)) (hf : s x) (hst : s t) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_at.comp_has_fderiv_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} (hg : g' (f x)) (hf : s x) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_within_at.comp_of_mem {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {s : set E} {g : F G} {g' : F →L[𝕜] G} {t : set F} (hg : t (f x)) (hf : s x) (hst : s) (nhds_within (f x) t)) :
has_fderiv_within_at (g f) (g'.comp f') s x
theorem has_fderiv_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {g : F G} {g' : F →L[𝕜] G} (hg : g' (f x)) (hf : f' x) :
has_fderiv_at (g f) (g'.comp f') x

The chain rule.

theorem differentiable_within_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : (f x)) (hf : x) (h : s t) :
(g f) s x
theorem differentiable_within_at.comp' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : (f x)) (hf : x) :
(g f) (s f ⁻¹' t) x
theorem differentiable_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {g : F G} (hg : (f x)) (hf : x) :
(g f) x
theorem differentiable_at.comp_differentiable_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {s : set E} {g : F G} (hg : (f x)) (hf : x) :
(g f) s x
theorem fderiv_within.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {s : set E} {g : F G} {t : set F} (hg : (f x)) (hf : x) (h : s t) (hxs : x) :
(g f) s x = g t (f x)).comp f s x)
theorem fderiv_within_fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {g : F G} {f : E F} {x : E} {y : F} {s : set E} {t : set F} (hg : y) (hf : x) (h : s t) (hxs : x) (hy : f x = y) (v : E) :
g t y) ( f s x) v) = (g f) s x) v

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.

theorem fderiv_within.comp₃ {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {G' : Type u_5} [ G'] {f : E F} (x : E) {s : set E} {g' : G G'} {g : F G} {t : set F} {u : set G} {y : F} {y' : G} (hg' : u y') (hg : y) (hf : x) (h2g : t u) (h2f : s t) (h3g : g y = y') (h3f : f x = y) (hxs : x) :
(g' g f) s x = g' u y').comp g t y).comp f s x))

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.

theorem fderiv.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {g : F G} (hg : (f x)) (hf : x) :
(g f) x = (fderiv 𝕜 g (f x)).comp (fderiv 𝕜 f x)
theorem fderiv.comp_fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} (x : E) {s : set E} {g : F G} (hg : (f x)) (hf : x) (hxs : x) :
(g f) s x = (fderiv 𝕜 g (f x)).comp f s x)
theorem differentiable_on.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {s : set E} {g : F G} {t : set F} (hg : t) (hf : s) (st : s t) :
(g f) s
theorem differentiable.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {g : F G} (hg : g) (hf : f) :
(g f)
theorem differentiable.comp_differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {s : set E} {g : F G} (hg : g) (hf : s) :
(g f) s
@[protected]
theorem has_strict_fderiv_at.comp {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] {f : E F} {f' : E →L[𝕜] F} (x : E) {g : F G} {g' : F →L[𝕜] G} (hg : (f x)) (hf : x) :
has_strict_fderiv_at (λ (x : E), g (f x)) (g'.comp f') x

The chain rule for derivatives in the sense of strict differentiability.

@[protected]
theorem differentiable.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {f : E E} (hf : f) (n : ) :
@[protected]
theorem differentiable_on.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {s : set E} {f : E E} (hf : s) (hs : s s) (n : ) :
s
@[protected]
theorem has_fderiv_at_filter.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {L : filter E} {f : E E} {f' : E →L[𝕜] E} (hf : x L) (hL : L) (hx : f x = x) (n : ) :
(f' ^ n) x L
@[protected]
theorem has_fderiv_at.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {f : E E} {f' : E →L[𝕜] E} (hf : f' x) (hx : f x = x) (n : ) :
(f' ^ n) x
@[protected]
theorem has_fderiv_within_at.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {f : E E} {f' : E →L[𝕜] E} (hf : s x) (hx : f x = x) (hs : s s) (n : ) :
(f' ^ n) s x
@[protected]
theorem has_strict_fderiv_at.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {f : E E} {f' : E →L[𝕜] E} (hf : x) (hx : f x = x) (n : ) :
(f' ^ n) x
@[protected]
theorem differentiable_at.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {f : E E} (hf : x) (hx : f x = x) (n : ) :
x
@[protected]
theorem differentiable_within_at.iterate {𝕜 : Type u_1} {E : Type u_2} [ E] {x : E} {s : set E} {f : E E} (hf : x) (hx : f x = x) (hs : s s) (n : ) :
x