One-dimensional derivatives of compositions of functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove the chain rule for the following cases:
has_deriv_at.competc:f : 𝕜' → 𝕜'composed withg : 𝕜 → 𝕜';has_deriv_at.scompetc:f : 𝕜' → Ecomposed withg : 𝕜 → 𝕜';has_fderiv_at.comp_has_deriv_atetc: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
has_deriv_at_filter.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{L : filter 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
{L' : filter 𝕜'}
(hg : has_deriv_at_filter g₁ g₁' (h x) L')
(hh : has_deriv_at_filter h h' x L)
(hL : filter.tendsto h L L') :
has_deriv_at_filter (g₁ ∘ h) (h' • g₁') x L
theorem
has_deriv_within_at.scomp_has_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{s' : set 𝕜'}
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
(hg : has_deriv_within_at g₁ g₁' s' (h x))
(hh : has_deriv_at h h' x)
(hs : ∀ (x : 𝕜), h x ∈ s') :
has_deriv_at (g₁ ∘ h) (h' • g₁') x
theorem
has_deriv_within_at.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{t' : set 𝕜'}
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
(hg : has_deriv_within_at g₁ g₁' t' (h x))
(hh : has_deriv_within_at h h' s x)
(hst : set.maps_to h s t') :
has_deriv_within_at (g₁ ∘ h) (h' • g₁') s x
theorem
has_deriv_at.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
(hg : has_deriv_at g₁ g₁' (h x))
(hh : has_deriv_at h h' x) :
has_deriv_at (g₁ ∘ h) (h' • g₁') x
The chain rule.
theorem
has_strict_deriv_at.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
(hg : has_strict_deriv_at g₁ g₁' (h x))
(hh : has_strict_deriv_at h h' x) :
has_strict_deriv_at (g₁ ∘ h) (h' • g₁') x
theorem
has_deriv_at.scomp_has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{h : 𝕜 → 𝕜'}
{h' : 𝕜'}
{g₁ : 𝕜' → F}
{g₁' : F}
(hg : has_deriv_at g₁ g₁' (h x))
(hh : has_deriv_within_at h h' s x) :
has_deriv_within_at (g₁ ∘ h) (h' • g₁') s x
theorem
deriv_within.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{t' : set 𝕜'}
{h : 𝕜 → 𝕜'}
{g₁ : 𝕜' → F}
(hg : differentiable_within_at 𝕜' g₁ t' (h x))
(hh : differentiable_within_at 𝕜 h s x)
(hs : set.maps_to h s t')
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (g₁ ∘ h) s x = deriv_within h s x • deriv_within g₁ t' (h x)
theorem
deriv.scomp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{h : 𝕜 → 𝕜'}
{g₁ : 𝕜' → F}
(hg : differentiable_at 𝕜' g₁ (h x))
(hh : differentiable_at 𝕜 h x) :
Derivative of the composition of a scalar and vector functions #
theorem
has_deriv_at_filter.comp_has_fderiv_at_filter
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h₂ : 𝕜' → 𝕜'}
{h₂' : 𝕜'}
{L' : filter 𝕜'}
{f : E → 𝕜'}
{f' : E →L[𝕜] 𝕜'}
(x : E)
{L'' : filter E}
(hh₂ : has_deriv_at_filter h₂ h₂' (f x) L')
(hf : has_fderiv_at_filter f f' x L'')
(hL : filter.tendsto f L'' L') :
has_fderiv_at_filter (h₂ ∘ f) (h₂' • f') x L''
theorem
has_strict_deriv_at.comp_has_strict_fderiv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h₂ : 𝕜' → 𝕜'}
{h₂' : 𝕜'}
{f : E → 𝕜'}
{f' : E →L[𝕜] 𝕜'}
(x : E)
(hh : has_strict_deriv_at h₂ h₂' (f x))
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (h₂ ∘ f) (h₂' • f') x
theorem
has_deriv_at.comp_has_fderiv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h₂ : 𝕜' → 𝕜'}
{h₂' : 𝕜'}
{f : E → 𝕜'}
{f' : E →L[𝕜] 𝕜'}
(x : E)
(hh : has_deriv_at h₂ h₂' (f x))
(hf : has_fderiv_at f f' x) :
has_fderiv_at (h₂ ∘ f) (h₂' • f') x
theorem
has_deriv_at.comp_has_fderiv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h₂ : 𝕜' → 𝕜'}
{h₂' : 𝕜'}
{f : E → 𝕜'}
{f' : E →L[𝕜] 𝕜'}
{s : set E}
(x : E)
(hh : has_deriv_at h₂ h₂' (f x))
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (h₂ ∘ f) (h₂' • f') s x
theorem
has_deriv_within_at.comp_has_fderiv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h₂ : 𝕜' → 𝕜'}
{h₂' : 𝕜'}
{f : E → 𝕜'}
{f' : E →L[𝕜] 𝕜'}
{s : set E}
{t : set 𝕜'}
(x : E)
(hh : has_deriv_within_at h₂ h₂' t (f x))
(hf : has_fderiv_within_at f f' s x)
(hst : set.maps_to f s t) :
has_fderiv_within_at (h₂ ∘ f) (h₂' • f') s x
Derivative of the composition of two scalar functions #
theorem
has_deriv_at_filter.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{L : filter 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
{h' h₂' : 𝕜'}
{L' : filter 𝕜'}
(hh₂ : has_deriv_at_filter h₂ h₂' (h x) L')
(hh : has_deriv_at_filter h h' x L)
(hL : filter.tendsto h L L') :
has_deriv_at_filter (h₂ ∘ h) (h₂' * h') x L
theorem
has_deriv_within_at.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{s' : set 𝕜'}
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
{h' h₂' : 𝕜'}
(hh₂ : has_deriv_within_at h₂ h₂' s' (h x))
(hh : has_deriv_within_at h h' s x)
(hst : set.maps_to h s s') :
has_deriv_within_at (h₂ ∘ h) (h₂' * h') s x
theorem
has_deriv_at.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
{h' h₂' : 𝕜'}
(hh₂ : has_deriv_at h₂ h₂' (h x))
(hh : has_deriv_at h h' x) :
has_deriv_at (h₂ ∘ h) (h₂' * h') x
The chain rule.
theorem
has_strict_deriv_at.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
{h' h₂' : 𝕜'}
(hh₂ : has_strict_deriv_at h₂ h₂' (h x))
(hh : has_strict_deriv_at h h' x) :
has_strict_deriv_at (h₂ ∘ h) (h₂' * h') x
theorem
has_deriv_at.comp_has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
{h' h₂' : 𝕜'}
(hh₂ : has_deriv_at h₂ h₂' (h x))
(hh : has_deriv_within_at h h' s x) :
has_deriv_within_at (h₂ ∘ h) (h₂' * h') s x
theorem
deriv_within.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{s' : set 𝕜'}
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
(hh₂ : differentiable_within_at 𝕜' h₂ s' (h x))
(hh : differentiable_within_at 𝕜 h s x)
(hs : set.maps_to h s s')
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (h₂ ∘ h) s x = deriv_within h₂ s' (h x) * deriv_within h s x
theorem
deriv.comp
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{h : 𝕜 → 𝕜'}
{h₂ : 𝕜' → 𝕜'}
(hh₂ : differentiable_at 𝕜' h₂ (h x))
(hh : differentiable_at 𝕜 h x) :
@[protected]
theorem
has_deriv_at_filter.iterate
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{L : filter 𝕜}
{f : 𝕜 → 𝕜}
{f' : 𝕜}
(hf : has_deriv_at_filter f f' x L)
(hL : filter.tendsto f L L)
(hx : f x = x)
(n : ℕ) :
has_deriv_at_filter f^[n] (f' ^ n) x L
@[protected]
theorem
has_deriv_at.iterate
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{f : 𝕜 → 𝕜}
{f' : 𝕜}
(hf : has_deriv_at f f' x)
(hx : f x = x)
(n : ℕ) :
has_deriv_at f^[n] (f' ^ n) x
@[protected]
theorem
has_deriv_within_at.iterate
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{s : set 𝕜}
{f : 𝕜 → 𝕜}
{f' : 𝕜}
(hf : has_deriv_within_at f f' s x)
(hx : f x = x)
(hs : set.maps_to f s s)
(n : ℕ) :
has_deriv_within_at f^[n] (f' ^ n) s x
@[protected]
theorem
has_strict_deriv_at.iterate
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
(x : 𝕜)
{f : 𝕜 → 𝕜}
{f' : 𝕜}
(hf : has_strict_deriv_at f f' x)
(hx : f x = x)
(n : ℕ) :
has_strict_deriv_at f^[n] (f' ^ n) x
Derivative of the composition of a function between vector spaces and a function on 𝕜 #
theorem
has_fderiv_within_at.comp_has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
{f' : F}
(x : 𝕜)
{s : set 𝕜}
{l : F → E}
{l' : F →L[𝕜] E}
{t : set F}
(hl : has_fderiv_within_at l l' t (f x))
(hf : has_deriv_within_at f f' s x)
(hst : set.maps_to f s t) :
has_deriv_within_at (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
has_fderiv_at.comp_has_deriv_within_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
{f' : F}
(x : 𝕜)
{s : set 𝕜}
{l : F → E}
{l' : F →L[𝕜] E}
(hl : has_fderiv_at l l' (f x))
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (l ∘ f) (⇑l' f') s x
theorem
has_fderiv_at.comp_has_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
{f' : F}
(x : 𝕜)
{l : F → E}
{l' : F →L[𝕜] E}
(hl : has_fderiv_at l l' (f x))
(hf : has_deriv_at f f' x) :
has_deriv_at (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
has_strict_fderiv_at.comp_has_strict_deriv_at
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
{f' : F}
(x : 𝕜)
{l : F → E}
{l' : F →L[𝕜] E}
(hl : has_strict_fderiv_at l l' (f x))
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (l ∘ f) (⇑l' f') x
theorem
fderiv_within.comp_deriv_within
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
(x : 𝕜)
{s : set 𝕜}
{l : F → E}
{t : set F}
(hl : differentiable_within_at 𝕜 l t (f x))
(hf : differentiable_within_at 𝕜 f s x)
(hs : set.maps_to f s t)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (l ∘ f) s x = ⇑(fderiv_within 𝕜 l t (f x)) (deriv_within f s x)
theorem
fderiv.comp_deriv
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{E : Type w}
[normed_add_comm_group E]
[normed_space 𝕜 E]
{f : 𝕜 → F}
(x : 𝕜)
{l : F → E}
(hl : differentiable_at 𝕜 l (f x))
(hf : differentiable_at 𝕜 f x) :