# Documentation

Mathlib.Analysis.Calculus.FDeriv.Comp

# The derivative of a composition (chain rule) #

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 HasFDerivAtFilter.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {L : } {g : FG} {g' : F →L[𝕜] G} {L' : } (hg : HasFDerivAtFilter g g' (f x) L') (hf : HasFDerivAtFilter f f' x L) (hL : Filter.Tendsto f L L') :
HasFDerivAtFilter (g f) () x L
theorem HasFDerivWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {s : Set E} {g : FG} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : Set.MapsTo f s t) :
HasFDerivWithinAt (g f) () s x
theorem HasFDerivAt.comp_hasFDerivWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {s : Set E} {g : FG} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (g f) () s x
theorem HasFDerivWithinAt.comp_of_mem {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {s : Set E} {g : FG} {g' : F →L[𝕜] G} {t : Set F} (hg : HasFDerivWithinAt g g' t (f x)) (hf : HasFDerivWithinAt f f' s x) (hst : Filter.Tendsto f () (nhdsWithin (f x) t)) :
HasFDerivWithinAt (g f) () s x
theorem HasFDerivAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {g : FG} {g' : F →L[𝕜] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) :
HasFDerivAt (g f) () x

The chain rule.

theorem DifferentiableWithinAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {s : Set E} {g : FG} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : ) (h : Set.MapsTo f s t) :
theorem DifferentiableWithinAt.comp' {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {s : Set E} {g : FG} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : ) :
DifferentiableWithinAt 𝕜 (g f) (s f ⁻¹' t) x
theorem DifferentiableAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {g : FG} (hg : DifferentiableAt 𝕜 g (f x)) (hf : ) :
DifferentiableAt 𝕜 (g f) x
theorem DifferentiableAt.comp_differentiableWithinAt {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {s : Set E} {g : FG} (hg : DifferentiableAt 𝕜 g (f x)) (hf : ) :
theorem fderivWithin.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {s : Set E} {g : FG} {t : Set F} (hg : DifferentiableWithinAt 𝕜 g t (f x)) (hf : ) (h : Set.MapsTo f s t) (hxs : ) :
fderivWithin 𝕜 (g f) s x = ContinuousLinearMap.comp (fderivWithin 𝕜 g t (f x)) (fderivWithin 𝕜 f s x)
theorem fderivWithin_fderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {g : FG} {f : EF} {x : E} {y : F} {s : Set E} {t : Set F} (hg : ) (hf : ) (h : Set.MapsTo f s t) (hxs : ) (hy : f x = y) (v : E) :
↑(fderivWithin 𝕜 g t y) (↑(fderivWithin 𝕜 f s x) v) = ↑(fderivWithin 𝕜 (g f) s x) v

A version of fderivWithin.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 fderivWithin.comp₃ {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {G' : Type u_5} [] [NormedSpace 𝕜 G'] {f : EF} (x : E) {s : Set E} {g' : GG'} {g : FG} {t : Set F} {u : Set G} {y : F} {y' : G} (hg' : DifferentiableWithinAt 𝕜 g' u y') (hg : ) (hf : ) (h2g : Set.MapsTo g t u) (h2f : Set.MapsTo f s t) (h3g : g y = y') (h3f : f x = y) (hxs : ) :
fderivWithin 𝕜 (g' g f) s x = ContinuousLinearMap.comp (fderivWithin 𝕜 g' u y') (ContinuousLinearMap.comp (fderivWithin 𝕜 g t y) (fderivWithin 𝕜 f s x))

Ternary version of fderivWithin.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} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {g : FG} (hg : DifferentiableAt 𝕜 g (f x)) (hf : ) :
fderiv 𝕜 (g f) x = ContinuousLinearMap.comp (fderiv 𝕜 g (f x)) (fderiv 𝕜 f x)
theorem fderiv.comp_fderivWithin {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} (x : E) {s : Set E} {g : FG} (hg : DifferentiableAt 𝕜 g (f x)) (hf : ) (hxs : ) :
fderivWithin 𝕜 (g f) s x = ContinuousLinearMap.comp (fderiv 𝕜 g (f x)) (fderivWithin 𝕜 f s x)
theorem DifferentiableOn.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {s : Set E} {g : FG} {t : Set F} (hg : ) (hf : ) (st : Set.MapsTo f s t) :
DifferentiableOn 𝕜 (g f) s
theorem Differentiable.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {g : FG} (hg : ) (hf : ) :
Differentiable 𝕜 (g f)
theorem Differentiable.comp_differentiableOn {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {s : Set E} {g : FG} (hg : ) (hf : ) :
DifferentiableOn 𝕜 (g f) s
theorem HasStrictFDerivAt.comp {𝕜 : Type u_1} {E : Type u_2} [] {F : Type u_3} [] {G : Type u_4} [] {f : EF} {f' : E →L[𝕜] F} (x : E) {g : FG} {g' : F →L[𝕜] G} (hg : HasStrictFDerivAt g g' (f x)) (hf : ) :
HasStrictFDerivAt (fun x => g (f x)) () x

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

theorem Differentiable.iterate {𝕜 : Type u_1} {E : Type u_2} [] {f : EE} (hf : ) (n : ) :
theorem DifferentiableOn.iterate {𝕜 : Type u_1} {E : Type u_2} [] {s : Set E} {f : EE} (hf : ) (hs : Set.MapsTo f s s) (n : ) :
theorem HasFDerivAtFilter.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {L : } {f : EE} {f' : E →L[𝕜] E} (hf : HasFDerivAtFilter f f' x L) (hL : ) (hx : f x = x) (n : ) :
HasFDerivAtFilter f^[n] (f' ^ n) x L
theorem HasFDerivAt.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {f : EE} {f' : E →L[𝕜] E} (hf : HasFDerivAt f f' x) (hx : f x = x) (n : ) :
HasFDerivAt f^[n] (f' ^ n) x
theorem HasFDerivWithinAt.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {s : Set E} {f : EE} {f' : E →L[𝕜] E} (hf : HasFDerivWithinAt f f' s x) (hx : f x = x) (hs : Set.MapsTo f s s) (n : ) :
HasFDerivWithinAt f^[n] (f' ^ n) s x
theorem HasStrictFDerivAt.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {f : EE} {f' : E →L[𝕜] E} (hf : ) (hx : f x = x) (n : ) :
theorem DifferentiableAt.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {f : EE} (hf : ) (hx : f x = x) (n : ) :
theorem DifferentiableWithinAt.iterate {𝕜 : Type u_1} {E : Type u_2} [] {x : E} {s : Set E} {f : EE} (hf : ) (hx : f x = x) (hs : Set.MapsTo f s s) (n : ) :