The derivative of a composition (chain rule) #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
has_fderiv_at_filter.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{L : filter E}
{g : F → G}
{g' : F →L[𝕜] G}
{L' : filter F}
(hg : has_fderiv_at_filter g g' (f x) L')
(hf : has_fderiv_at_filter f f' x L)
(hL : filter.tendsto f L L') :
has_fderiv_at_filter (g ∘ f) (g'.comp f') x L
theorem
has_fderiv_within_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{s : set E}
{g : F → G}
{g' : F →L[𝕜] G}
{t : set F}
(hg : has_fderiv_within_at g g' t (f x))
(hf : has_fderiv_within_at f f' s x)
(hst : set.maps_to f s t) :
has_fderiv_within_at (g ∘ f) (g'.comp f') s x
theorem
has_fderiv_at.comp_has_fderiv_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{s : set E}
{g : F → G}
{g' : F →L[𝕜] G}
(hg : has_fderiv_at g g' (f x))
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (g ∘ f) (g'.comp f') s x
theorem
has_fderiv_within_at.comp_of_mem
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{s : set E}
{g : F → G}
{g' : F →L[𝕜] G}
{t : set F}
(hg : has_fderiv_within_at g g' t (f x))
(hf : has_fderiv_within_at f f' s x)
(hst : filter.tendsto f (nhds_within x s) (nhds_within (f x) t)) :
has_fderiv_within_at (g ∘ f) (g'.comp f') s x
theorem
has_fderiv_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{g : F → G}
{g' : F →L[𝕜] G}
(hg : has_fderiv_at g g' (f x))
(hf : has_fderiv_at f f' x) :
has_fderiv_at (g ∘ f) (g'.comp f') x
The chain rule.
theorem
differentiable_within_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{s : set E}
{g : F → G}
{t : set F}
(hg : differentiable_within_at 𝕜 g t (f x))
(hf : differentiable_within_at 𝕜 f s x)
(h : set.maps_to f s t) :
differentiable_within_at 𝕜 (g ∘ f) s x
theorem
differentiable_within_at.comp'
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{s : set E}
{g : F → G}
{t : set F}
(hg : differentiable_within_at 𝕜 g t (f x))
(hf : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x
theorem
differentiable_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{g : F → G}
(hg : differentiable_at 𝕜 g (f x))
(hf : differentiable_at 𝕜 f x) :
differentiable_at 𝕜 (g ∘ f) x
theorem
differentiable_at.comp_differentiable_within_at
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{s : set E}
{g : F → G}
(hg : differentiable_at 𝕜 g (f x))
(hf : differentiable_within_at 𝕜 f s x) :
differentiable_within_at 𝕜 (g ∘ f) s x
theorem
fderiv_within.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{s : set E}
{g : F → G}
{t : set F}
(hg : differentiable_within_at 𝕜 g t (f x))
(hf : differentiable_within_at 𝕜 f s x)
(h : set.maps_to f s t)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g ∘ f) s x = (fderiv_within 𝕜 g t (f x)).comp (fderiv_within 𝕜 f s x)
theorem
fderiv_within_fderiv_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{g : F → G}
{f : E → F}
{x : E}
{y : F}
{s : set E}
{t : set F}
(hg : differentiable_within_at 𝕜 g t y)
(hf : differentiable_within_at 𝕜 f s x)
(h : set.maps_to f s t)
(hxs : unique_diff_within_at 𝕜 s x)
(hy : f x = y)
(v : E) :
⇑(fderiv_within 𝕜 g t y) (⇑(fderiv_within 𝕜 f s x) v) = ⇑(fderiv_within 𝕜 (g ∘ f) s x) v
A version of fderiv_within.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
fderiv_within.comp₃
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{G' : Type u_5}
[normed_add_comm_group G']
[normed_space 𝕜 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' : differentiable_within_at 𝕜 g' u y')
(hg : differentiable_within_at 𝕜 g t y)
(hf : differentiable_within_at 𝕜 f s x)
(h2g : set.maps_to g t u)
(h2f : set.maps_to f s t)
(h3g : g y = y')
(h3f : f x = y)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g' ∘ g ∘ f) s x = (fderiv_within 𝕜 g' u y').comp ((fderiv_within 𝕜 g t y).comp (fderiv_within 𝕜 f s x))
Ternary version of fderiv_within.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}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{g : F → G}
(hg : differentiable_at 𝕜 g (f x))
(hf : differentiable_at 𝕜 f x) :
theorem
fderiv.comp_fderiv_within
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
(x : E)
{s : set E}
{g : F → G}
(hg : differentiable_at 𝕜 g (f x))
(hf : differentiable_within_at 𝕜 f s x)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (fderiv_within 𝕜 f s x)
theorem
differentiable_on.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{s : set E}
{g : F → G}
{t : set F}
(hg : differentiable_on 𝕜 g t)
(hf : differentiable_on 𝕜 f s)
(st : set.maps_to f s t) :
differentiable_on 𝕜 (g ∘ f) s
theorem
differentiable.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{g : F → G}
(hg : differentiable 𝕜 g)
(hf : differentiable 𝕜 f) :
differentiable 𝕜 (g ∘ f)
theorem
differentiable.comp_differentiable_on
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{s : set E}
{g : F → G}
(hg : differentiable 𝕜 g)
(hf : differentiable_on 𝕜 f s) :
differentiable_on 𝕜 (g ∘ f) s
@[protected]
theorem
has_strict_fderiv_at.comp
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{F : Type u_3}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{G : Type u_4}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{f : E → F}
{f' : E →L[𝕜] F}
(x : E)
{g : F → G}
{g' : F →L[𝕜] G}
(hg : has_strict_fderiv_at g g' (f x))
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), g (f x)) (g'.comp f') x
The chain rule for derivatives in the sense of strict differentiability.
@[protected]
theorem
differentiable.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : E → E}
(hf : differentiable 𝕜 f)
(n : ℕ) :
differentiable 𝕜 f^[n]
@[protected]
theorem
differentiable_on.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{s : set E}
{f : E → E}
(hf : differentiable_on 𝕜 f s)
(hs : set.maps_to f s s)
(n : ℕ) :
differentiable_on 𝕜 f^[n] s
@[protected]
theorem
has_fderiv_at_filter.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{L : filter E}
{f : E → E}
{f' : E →L[𝕜] E}
(hf : has_fderiv_at_filter f f' x L)
(hL : filter.tendsto f L L)
(hx : f x = x)
(n : ℕ) :
has_fderiv_at_filter f^[n] (f' ^ n) x L
@[protected]
theorem
has_fderiv_at.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{f : E → E}
{f' : E →L[𝕜] E}
(hf : has_fderiv_at f f' x)
(hx : f x = x)
(n : ℕ) :
has_fderiv_at f^[n] (f' ^ n) x
@[protected]
theorem
has_fderiv_within_at.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{f : E → E}
{f' : E →L[𝕜] E}
(hf : has_fderiv_within_at f f' s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : ℕ) :
has_fderiv_within_at f^[n] (f' ^ n) s x
@[protected]
theorem
has_strict_fderiv_at.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{f : E → E}
{f' : E →L[𝕜] E}
(hf : has_strict_fderiv_at f f' x)
(hx : f x = x)
(n : ℕ) :
has_strict_fderiv_at f^[n] (f' ^ n) x
@[protected]
theorem
differentiable_at.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{f : E → E}
(hf : differentiable_at 𝕜 f x)
(hx : f x = x)
(n : ℕ) :
differentiable_at 𝕜 f^[n] x
@[protected]
theorem
differentiable_within_at.iterate
{𝕜 : Type u_1}
[nontrivially_normed_field 𝕜]
{E : Type u_2}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{x : E}
{s : set E}
{f : E → E}
(hf : differentiable_within_at 𝕜 f s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : ℕ) :
differentiable_within_at 𝕜 f^[n] s x