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) (g'.comp 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) (g'.comp 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) (g'.comp f') s x
theorem
HasFDerivWithinAt.comp_of_tendsto
{𝕜 : 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) (g'.comp f') s x
@[deprecated HasFDerivWithinAt.comp_of_tendsto]
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) (g'.comp f') s x
Alias of HasFDerivWithinAt.comp_of_tendsto.
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) (g'.comp 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 = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
@[deprecated fderivWithin_comp]
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 = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
Alias of fderivWithin_comp.
theorem
fderivWithin_comp_of_eq
{𝕜 : 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}
{y : 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)
:
fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 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 𝕜 (fun (y : E) => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
A variant for the derivative of a composition, written without ∘.
theorem
fderivWithin_comp_of_eq'
{𝕜 : 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}
{y : 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)
:
fderivWithin 𝕜 (fun (y : E) => g (f y)) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
A variant for the derivative of a composition, written without ∘.
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 = (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.
@[deprecated fderivWithin_comp₃]
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 = (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (fderivWithin 𝕜 f s x))
Alias of fderivWithin_comp₃.
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)
:
@[deprecated fderiv_comp]
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)
:
Alias of fderiv_comp.
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)
:
A variant for the derivative of a composition, written without ∘.
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 = (fderiv 𝕜 g (f x)).comp (fderivWithin 𝕜 f s x)
@[deprecated fderiv_comp_fderivWithin]
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 = (fderiv 𝕜 g (f x)).comp (fderivWithin 𝕜 f s x)
Alias of fderiv_comp_fderivWithin.
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)) (g'.comp 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