# 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} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {L : } {g : F β G} {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) (g'.comp f') x L
theorem HasFDerivWithinAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : Set E} {g : F β G} {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) (g'.comp f') s x
theorem HasFDerivAt.comp_hasFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : Set E} {g : F β G} {g' : F βL[π] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (g β f) (g'.comp f') s x
theorem HasFDerivWithinAt.comp_of_mem {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {s : Set E} {g : F β G} {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) (g'.comp f') s x
theorem HasFDerivAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {g : F β G} {g' : F βL[π] G} (hg : HasFDerivAt g g' (f x)) (hf : HasFDerivAt f f' x) :
HasFDerivAt (g β f) (g'.comp f') x

The chain rule.

theorem DifferentiableWithinAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {s : Set E} {g : F β G} {t : Set F} (hg : DifferentiableWithinAt π g t (f x)) (hf : DifferentiableWithinAt π f s x) (h : Set.MapsTo f s t) :
DifferentiableWithinAt π (g β f) s x
theorem DifferentiableWithinAt.comp' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {s : Set E} {g : F β G} {t : Set F} (hg : DifferentiableWithinAt π g t (f x)) (hf : DifferentiableWithinAt π f s x) :
theorem DifferentiableAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {g : F β G} (hg : DifferentiableAt π g (f x)) (hf : DifferentiableAt π f x) :
DifferentiableAt π (g β f) x
theorem DifferentiableAt.comp_differentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {s : Set E} {g : F β G} (hg : DifferentiableAt π g (f x)) (hf : DifferentiableWithinAt π f s x) :
DifferentiableWithinAt π (g β f) s x
theorem fderivWithin.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {s : Set E} {g : F β G} {t : Set F} (hg : DifferentiableWithinAt π g t (f x)) (hf : DifferentiableWithinAt π f s x) (h : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π (g β f) s x = (fderivWithin π g t (f x)).comp (fderivWithin π f s x)
theorem fderivWithin_fderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {g : F β G} {f : E β F} {x : E} {y : F} {s : Set E} {t : Set F} (hg : DifferentiableWithinAt π g t y) (hf : DifferentiableWithinAt π f s x) (h : Set.MapsTo f s t) (hxs : UniqueDiffWithinAt π s x) (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} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [NormedSpace π 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' : DifferentiableWithinAt π g' u y') (hg : DifferentiableWithinAt π g t y) (hf : DifferentiableWithinAt π f s x) (h2g : Set.MapsTo g t u) (h2f : Set.MapsTo f s t) (h3g : g y = y') (h3f : f x = y) (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π (g' β g β f) s x = (fderivWithin π g' u y').comp ((fderivWithin π g t y).comp (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} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {g : F β G} (hg : DifferentiableAt π g (f x)) (hf : DifferentiableAt π f x) :
fderiv π (g β f) x = (fderiv π g (f x)).comp (fderiv π f x)
theorem fderiv.comp_fderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} (x : E) {s : Set E} {g : F β G} (hg : DifferentiableAt π g (f x)) (hf : DifferentiableWithinAt π f s x) (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π (g β f) s x = (fderiv π g (f x)).comp (fderivWithin π f s x)
theorem DifferentiableOn.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {s : Set E} {g : F β G} {t : Set F} (hg : DifferentiableOn π g t) (hf : DifferentiableOn π f s) (st : Set.MapsTo f s t) :
DifferentiableOn π (g β f) s
theorem Differentiable.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {g : F β G} (hg : Differentiable π g) (hf : Differentiable π f) :
Differentiable π (g β f)
theorem Differentiable.comp_differentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {s : Set E} {g : F β G} (hg : Differentiable π g) (hf : DifferentiableOn π f s) :
DifferentiableOn π (g β f) s
theorem HasStrictFDerivAt.comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {f : E β F} {f' : E βL[π] F} (x : E) {g : F β G} {g' : F βL[π] G} (hg : HasStrictFDerivAt g g' (f x)) (hf : ) :
HasStrictFDerivAt (fun (x : E) => g (f x)) (g'.comp f') x

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

theorem Differentiable.iterate {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {f : E β E} (hf : Differentiable π f) (n : β) :
Differentiable π f^[n]
theorem DifferentiableOn.iterate {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {f : E β E} (hf : DifferentiableOn π f s) (hs : Set.MapsTo f s s) (n : β) :
DifferentiableOn π f^[n] s
theorem HasFDerivAtFilter.iterate {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {L : } {f : E β E} {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} [NormedSpace π E] {x : E} {f : E β E} {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} [NormedSpace π E] {x : E} {s : Set E} {f : E β E} {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} [NormedSpace π E] {x : E} {f : E β E} {f' : E βL[π] E} (hf : ) (hx : f x = x) (n : β) :
theorem DifferentiableAt.iterate {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {f : E β E} (hf : DifferentiableAt π f x) (hx : f x = x) (n : β) :
DifferentiableAt π f^[n] x
theorem DifferentiableWithinAt.iterate {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {f : E β E} (hf : DifferentiableWithinAt π f s x) (hx : f x = x) (hs : Set.MapsTo f s s) (n : β) :