One-dimensional derivatives of compositions of functions #
In this file we prove the chain rule for the following cases:
HasDerivAt.competc:f : π' β π'composed withg : π β π';HasDerivAt.scompetc:f : π' β Ecomposed withg : π β π';HasFDerivAt.comp_hasDerivAtetc:f : E β Fcomposed withg : π β E;
Here π is the base normed field, E and F are normed spaces over π and π' is an algebra
over π (e.g., π'=π or π=β, π'=β).
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
analysis/calculus/deriv/basic.
Keywords #
derivative, chain rule
Derivative of the composition of a vector function and a scalar function #
We use scomp in lemmas on composition of vector valued and scalar valued functions, and comp
in lemmas on composition of scalar valued functions, in analogy for smul and mul (and also
because the comp version with the shorter name will show up much more often in applications).
The formula for the derivative involves smul in scomp lemmas, which can be reduced to
usual multiplication in comp lemmas.
theorem
HasDerivAtFilter.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{L : Filter π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
{L' : Filter π'}
(hg : HasDerivAtFilter gβ gβ' (h x) L')
(hh : HasDerivAtFilter h h' x L)
(hL : Filter.Tendsto h L L')
:
HasDerivAtFilter (gβ β h) (h' β’ gβ') x L
theorem
HasDerivWithinAt.scomp_hasDerivAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{s' : Set π'}
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
(hg : HasDerivWithinAt gβ gβ' s' (h x))
(hh : HasDerivAt h h' x)
(hs : β (x : π), h x β s')
:
HasDerivAt (gβ β h) (h' β’ gβ') x
theorem
HasDerivWithinAt.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{t' : Set π'}
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
(hg : HasDerivWithinAt gβ gβ' t' (h x))
(hh : HasDerivWithinAt h h' s x)
(hst : Set.MapsTo h s t')
:
HasDerivWithinAt (gβ β h) (h' β’ gβ') s x
theorem
HasDerivAt.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
(hg : HasDerivAt gβ gβ' (h x))
(hh : HasDerivAt h h' x)
:
HasDerivAt (gβ β h) (h' β’ gβ') x
The chain rule.
theorem
HasStrictDerivAt.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
(hg : HasStrictDerivAt gβ gβ' (h x))
(hh : HasStrictDerivAt h h' x)
:
HasStrictDerivAt (gβ β h) (h' β’ gβ') x
theorem
HasDerivAt.scomp_hasDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{h : π β π'}
{h' : π'}
{gβ : π' β F}
{gβ' : F}
(hg : HasDerivAt gβ gβ' (h x))
(hh : HasDerivWithinAt h h' s x)
:
HasDerivWithinAt (gβ β h) (h' β’ gβ') s x
theorem
derivWithin.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{t' : Set π'}
{h : π β π'}
{gβ : π' β F}
(hg : DifferentiableWithinAt π' gβ t' (h x))
(hh : DifferentiableWithinAt π h s x)
(hs : Set.MapsTo h s t')
(hxs : UniqueDiffWithinAt π s x)
:
derivWithin (gβ β h) s x = derivWithin h s x β’ derivWithin gβ t' (h x)
theorem
deriv.scomp
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
[NormedSpace π' F]
[IsScalarTower π π' F]
{h : π β π'}
{gβ : π' β F}
(hg : DifferentiableAt π' gβ (h x))
(hh : DifferentiableAt π h x)
:
Derivative of the composition of a scalar and vector functions #
theorem
HasDerivAtFilter.comp_hasFDerivAtFilter
{π : Type u}
[NontriviallyNormedField π]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{hβ : π' β π'}
{hβ' : π'}
{L' : Filter π'}
{f : E β π'}
{f' : E βL[π] π'}
(x : E)
{L'' : Filter E}
(hhβ : HasDerivAtFilter hβ hβ' (f x) L')
(hf : HasFDerivAtFilter f f' x L'')
(hL : Filter.Tendsto f L'' L')
:
HasFDerivAtFilter (hβ β f) (hβ' β’ f') x L''
theorem
HasStrictDerivAt.comp_hasStrictFDerivAt
{π : Type u}
[NontriviallyNormedField π]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{hβ : π' β π'}
{hβ' : π'}
{f : E β π'}
{f' : E βL[π] π'}
(x : E)
(hh : HasStrictDerivAt hβ hβ' (f x))
(hf : HasStrictFDerivAt f f' x)
:
HasStrictFDerivAt (hβ β f) (hβ' β’ f') x
theorem
HasDerivAt.comp_hasFDerivAt
{π : Type u}
[NontriviallyNormedField π]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{hβ : π' β π'}
{hβ' : π'}
{f : E β π'}
{f' : E βL[π] π'}
(x : E)
(hh : HasDerivAt hβ hβ' (f x))
(hf : HasFDerivAt f f' x)
:
HasFDerivAt (hβ β f) (hβ' β’ f') x
theorem
HasDerivAt.comp_hasFDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{hβ : π' β π'}
{hβ' : π'}
{f : E β π'}
{f' : E βL[π] π'}
{s : Set E}
(x : E)
(hh : HasDerivAt hβ hβ' (f x))
(hf : HasFDerivWithinAt f f' s x)
:
HasFDerivWithinAt (hβ β f) (hβ' β’ f') s x
theorem
HasDerivWithinAt.comp_hasFDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{hβ : π' β π'}
{hβ' : π'}
{f : E β π'}
{f' : E βL[π] π'}
{s : Set E}
{t : Set π'}
(x : E)
(hh : HasDerivWithinAt hβ hβ' t (f x))
(hf : HasFDerivWithinAt f f' s x)
(hst : Set.MapsTo f s t)
:
HasFDerivWithinAt (hβ β f) (hβ' β’ f') s x
Derivative of the composition of two scalar functions #
theorem
HasDerivAtFilter.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{L : Filter π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{h : π β π'}
{hβ : π' β π'}
{h' : π'}
{hβ' : π'}
{L' : Filter π'}
(hhβ : HasDerivAtFilter hβ hβ' (h x) L')
(hh : HasDerivAtFilter h h' x L)
(hL : Filter.Tendsto h L L')
:
HasDerivAtFilter (hβ β h) (hβ' * h') x L
theorem
HasDerivWithinAt.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{s' : Set π'}
{h : π β π'}
{hβ : π' β π'}
{h' : π'}
{hβ' : π'}
(hhβ : HasDerivWithinAt hβ hβ' s' (h x))
(hh : HasDerivWithinAt h h' s x)
(hst : Set.MapsTo h s s')
:
HasDerivWithinAt (hβ β h) (hβ' * h') s x
theorem
HasDerivAt.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{h : π β π'}
{hβ : π' β π'}
{h' : π'}
{hβ' : π'}
(hhβ : HasDerivAt hβ hβ' (h x))
(hh : HasDerivAt h h' x)
:
HasDerivAt (hβ β h) (hβ' * h') x
The chain rule.
theorem
HasStrictDerivAt.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{h : π β π'}
{hβ : π' β π'}
{h' : π'}
{hβ' : π'}
(hhβ : HasStrictDerivAt hβ hβ' (h x))
(hh : HasStrictDerivAt h h' x)
:
HasStrictDerivAt (hβ β h) (hβ' * h') x
theorem
HasDerivAt.comp_hasDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{h : π β π'}
{hβ : π' β π'}
{h' : π'}
{hβ' : π'}
(hhβ : HasDerivAt hβ hβ' (h x))
(hh : HasDerivWithinAt h h' s x)
:
HasDerivWithinAt (hβ β h) (hβ' * h') s x
theorem
derivWithin.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{s : Set π}
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{s' : Set π'}
{h : π β π'}
{hβ : π' β π'}
(hhβ : DifferentiableWithinAt π' hβ s' (h x))
(hh : DifferentiableWithinAt π h s x)
(hs : Set.MapsTo h s s')
(hxs : UniqueDiffWithinAt π s x)
:
derivWithin (hβ β h) s x = derivWithin hβ s' (h x) * derivWithin h s x
theorem
deriv.comp
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{π' : Type u_1}
[NontriviallyNormedField π']
[NormedAlgebra π π']
{h : π β π'}
{hβ : π' β π'}
(hhβ : DifferentiableAt π' hβ (h x))
(hh : DifferentiableAt π h x)
:
theorem
HasDerivAtFilter.iterate
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{L : Filter π}
{f : π β π}
{f' : π}
(hf : HasDerivAtFilter f f' x L)
(hL : Filter.Tendsto f L L)
(hx : f x = x)
(n : β)
:
HasDerivAtFilter f^[n] (f' ^ n) x L
theorem
HasDerivAt.iterate
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{f : π β π}
{f' : π}
(hf : HasDerivAt f f' x)
(hx : f x = x)
(n : β)
:
HasDerivAt f^[n] (f' ^ n) x
theorem
HasDerivWithinAt.iterate
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{s : Set π}
{f : π β π}
{f' : π}
(hf : HasDerivWithinAt f f' s x)
(hx : f x = x)
(hs : Set.MapsTo f s s)
(n : β)
:
HasDerivWithinAt f^[n] (f' ^ n) s x
theorem
HasStrictDerivAt.iterate
{π : Type u}
[NontriviallyNormedField π]
(x : π)
{f : π β π}
{f' : π}
(hf : HasStrictDerivAt f f' x)
(hx : f x = x)
(n : β)
:
HasStrictDerivAt f^[n] (f' ^ n) x
Derivative of the composition of a function between vector spaces and a function on π #
theorem
HasFDerivWithinAt.comp_hasDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
{f' : F}
(x : π)
{s : Set π}
{l : F β E}
{l' : F βL[π] E}
{t : Set F}
(hl : HasFDerivWithinAt l l' t (f x))
(hf : HasDerivWithinAt f f' s x)
(hst : Set.MapsTo f s t)
:
HasDerivWithinAt (l β f) (l' f') s x
The composition l β f where l : F β E and f : π β F, has a derivative within a set
equal to the FrΓ©chet derivative of l applied to the derivative of f.
theorem
HasFDerivAt.comp_hasDerivWithinAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
{f' : F}
(x : π)
{s : Set π}
{l : F β E}
{l' : F βL[π] E}
(hl : HasFDerivAt l l' (f x))
(hf : HasDerivWithinAt f f' s x)
:
HasDerivWithinAt (l β f) (l' f') s x
theorem
HasFDerivAt.comp_hasDerivAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
{f' : F}
(x : π)
{l : F β E}
{l' : F βL[π] E}
(hl : HasFDerivAt l l' (f x))
(hf : HasDerivAt f f' x)
:
HasDerivAt (l β f) (l' f') x
The composition l β f where l : F β E and f : π β F, has a derivative equal to the
FrΓ©chet derivative of l applied to the derivative of f.
theorem
HasStrictFDerivAt.comp_hasStrictDerivAt
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
{f' : F}
(x : π)
{l : F β E}
{l' : F βL[π] E}
(hl : HasStrictFDerivAt l l' (f x))
(hf : HasStrictDerivAt f f' x)
:
HasStrictDerivAt (l β f) (l' f') x
theorem
fderivWithin.comp_derivWithin
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
(x : π)
{s : Set π}
{l : F β E}
{t : Set F}
(hl : DifferentiableWithinAt π l t (f x))
(hf : DifferentiableWithinAt π f s x)
(hs : Set.MapsTo f s t)
(hxs : UniqueDiffWithinAt π s x)
:
derivWithin (l β f) s x = (fderivWithin π l t (f x)) (derivWithin f s x)
theorem
fderiv.comp_deriv
{π : Type u}
[NontriviallyNormedField π]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace π F]
{E : Type w}
[NormedAddCommGroup E]
[NormedSpace π E]
{f : π β F}
(x : π)
{l : F β E}
(hl : DifferentiableAt π l (f x))
(hf : DifferentiableAt π f x)
: