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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
{f : E β F}
{f' : E βL[π] F}
(x : E)
{L : Filter E}
{g : F β G}
{g' : F βL[π] G}
{L' : Filter F}
(hg : HasFDerivAtFilter g g' (f x) L')
(hf : HasFDerivAtFilter f f' x L)
(hL : Filter.Tendsto f L L')
:
HasFDerivAtFilter (g β f) (ContinuousLinearMap.comp g' f') x L
theorem
HasFDerivWithinAt.comp
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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) (ContinuousLinearMap.comp g' f') s x
theorem
HasFDerivAt.comp_hasFDerivWithinAt
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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) (ContinuousLinearMap.comp g' f') s x
theorem
HasFDerivWithinAt.comp_of_mem
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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 x s) (nhdsWithin (f x) t))
:
HasFDerivWithinAt (g β f) (ContinuousLinearMap.comp g' f') s x
theorem
HasFDerivAt.comp
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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) (ContinuousLinearMap.comp g' f') x
The chain rule.
theorem
DifferentiableWithinAt.comp
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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)
:
DifferentiableWithinAt π (g β f) (s β© f β»ΒΉ' t) x
theorem
DifferentiableAt.comp
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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 = ContinuousLinearMap.comp (fderivWithin π g t (f x)) (fderivWithin π f s x)
theorem
fderivWithin_fderivWithin
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
{G' : Type u_5}
[NormedAddCommGroup G']
[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 = 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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
{f : E β F}
(x : E)
{g : F β G}
(hg : DifferentiableAt π g (f x))
(hf : DifferentiableAt π f x)
:
theorem
fderiv.comp_fderivWithin
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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 = ContinuousLinearMap.comp (fderiv π g (f x)) (fderivWithin π f s x)
theorem
DifferentiableOn.comp
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[NormedSpace π G]
{f : E β F}
{g : F β G}
(hg : Differentiable π g)
(hf : Differentiable π f)
:
Differentiable π (g β f)
theorem
Differentiable.comp_differentiableOn
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace π F]
{G : Type u_4}
[NormedAddCommGroup G]
[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 f f' x)
:
HasStrictFDerivAt (fun (x : E) => g (f x)) (ContinuousLinearMap.comp g' f') x
The chain rule for derivatives in the sense of strict differentiability.
theorem
Differentiable.iterate
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : E β E}
(hf : Differentiable π f)
(n : β)
:
Differentiable π f^[n]
theorem
DifferentiableOn.iterate
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{x : E}
{L : Filter E}
{f : E β E}
{f' : E βL[π] E}
(hf : HasFDerivAtFilter f f' x L)
(hL : Filter.Tendsto f L L)
(hx : f x = x)
(n : β)
:
HasFDerivAtFilter f^[n] (f' ^ n) x L
theorem
HasFDerivAt.iterate
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace π E]
{x : E}
{f : E β E}
{f' : E βL[π] E}
(hf : HasStrictFDerivAt f f' x)
(hx : f x = x)
(n : β)
:
HasStrictFDerivAt f^[n] (f' ^ n) x
theorem
DifferentiableAt.iterate
{π : Type u_1}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[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}
[NontriviallyNormedField π]
{E : Type u_2}
[NormedAddCommGroup E]
[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 : β)
:
DifferentiableWithinAt π f^[n] s x