Derivative of f x * g x #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove formulas for (f x * g x)' and (f x • g x)'.
For a more detailed overview of one-dimensional derivatives in mathlib, see the module docstring of
analysis/calculus/deriv/basic.
Keywords #
derivative, multiplication
Derivative of the multiplication of a scalar function and a vector function #
theorem
has_deriv_within_at.smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_within_at c c' s x)
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (y : 𝕜), c y • f y) (c x • f' + c' • f x) s x
theorem
has_deriv_at.smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_at c c' x)
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (y : 𝕜), c y • f y) (c x • f' + c' • f x) x
theorem
has_strict_deriv_at.smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_strict_deriv_at c c' x)
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (y : 𝕜), c y • f y) (c x • f' + c' • f x) x
theorem
deriv_within_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : 𝕜 → 𝕜'}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hf : differentiable_within_at 𝕜 f s x) :
deriv_within (λ (y : 𝕜), c y • f y) s x = c x • deriv_within f s x + deriv_within c s x • f x
theorem
deriv_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
[normed_space 𝕜' F]
[is_scalar_tower 𝕜 𝕜' F]
{c : 𝕜 → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(hf : differentiable_at 𝕜 f x) :
theorem
has_strict_deriv_at.smul_const
{𝕜 : 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]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_strict_deriv_at c c' x)
(f : F) :
has_strict_deriv_at (λ (y : 𝕜), c y • f) (c' • f) x
theorem
has_deriv_within_at.smul_const
{𝕜 : 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]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_within_at c c' s x)
(f : F) :
has_deriv_within_at (λ (y : 𝕜), c y • f) (c' • f) s x
theorem
has_deriv_at.smul_const
{𝕜 : 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]
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_at c c' x)
(f : F) :
has_deriv_at (λ (y : 𝕜), c y • f) (c' • f) x
theorem
deriv_within_smul_const
{𝕜 : 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]
{c : 𝕜 → 𝕜'}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(f : F) :
deriv_within (λ (y : 𝕜), c y • f) s x = deriv_within c s x • f
theorem
deriv_smul_const
{𝕜 : 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]
{c : 𝕜 → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(f : F) :
theorem
has_strict_deriv_at.const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(c : R)
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (y : 𝕜), c • f y) (c • f') x
theorem
has_deriv_at_filter.const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{L : filter 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(c : R)
(hf : has_deriv_at_filter f f' x L) :
has_deriv_at_filter (λ (y : 𝕜), c • f y) (c • f') x L
theorem
has_deriv_within_at.const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{s : set 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(c : R)
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (y : 𝕜), c • f y) (c • f') s x
theorem
has_deriv_at.const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{f' : F}
{x : 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(c : R)
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (y : 𝕜), c • f y) (c • f') x
theorem
deriv_within_const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{s : set 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(hxs : unique_diff_within_at 𝕜 s x)
(c : R)
(hf : differentiable_within_at 𝕜 f s x) :
deriv_within (λ (y : 𝕜), c • f y) s x = c • deriv_within f s x
theorem
deriv_const_smul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{f : 𝕜 → F}
{x : 𝕜}
{R : Type u_1}
[semiring R]
[module R F]
[smul_comm_class 𝕜 R F]
[has_continuous_const_smul R F]
(c : R)
(hf : differentiable_at 𝕜 f x) :
Derivative of the multiplication of two functions #
theorem
has_deriv_within_at.mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
{c' d' : 𝔸}
(hc : has_deriv_within_at c c' s x)
(hd : has_deriv_within_at d d' s x) :
has_deriv_within_at (λ (y : 𝕜), c y * d y) (c' * d x + c x * d') s x
theorem
has_deriv_at.mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
{c' d' : 𝔸}
(hc : has_deriv_at c c' x)
(hd : has_deriv_at d d' x) :
has_deriv_at (λ (y : 𝕜), c y * d y) (c' * d x + c x * d') x
theorem
has_strict_deriv_at.mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
{c' d' : 𝔸}
(hc : has_strict_deriv_at c c' x)
(hd : has_strict_deriv_at d d' x) :
has_strict_deriv_at (λ (y : 𝕜), c y * d y) (c' * d x + c x * d') x
theorem
deriv_within_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x) :
deriv_within (λ (y : 𝕜), c y * d y) s x = deriv_within c s x * d x + c x * deriv_within d s x
@[simp]
theorem
deriv_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x) :
theorem
has_deriv_within_at.mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c : 𝕜 → 𝔸}
{c' : 𝔸}
(hc : has_deriv_within_at c c' s x)
(d : 𝔸) :
has_deriv_within_at (λ (y : 𝕜), c y * d) (c' * d) s x
theorem
has_deriv_at.mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c : 𝕜 → 𝔸}
{c' : 𝔸}
(hc : has_deriv_at c c' x)
(d : 𝔸) :
has_deriv_at (λ (y : 𝕜), c y * d) (c' * d) x
theorem
has_deriv_at_mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
(c : 𝕜) :
has_deriv_at (λ (x : 𝕜), x * c) c x
theorem
has_strict_deriv_at.mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c : 𝕜 → 𝔸}
{c' : 𝔸}
(hc : has_strict_deriv_at c c' x)
(d : 𝔸) :
has_strict_deriv_at (λ (y : 𝕜), c y * d) (c' * d) x
theorem
deriv_within_mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c : 𝕜 → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(d : 𝔸) :
deriv_within (λ (y : 𝕜), c y * d) s x = deriv_within c s x * d
theorem
deriv_mul_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{c : 𝕜 → 𝔸}
(hc : differentiable_at 𝕜 c x)
(d : 𝔸) :
theorem
deriv_mul_const_field
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{u : 𝕜 → 𝕜'}
(v : 𝕜') :
@[simp]
theorem
deriv_mul_const_field'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{𝕜' : Type u_1}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{u : 𝕜 → 𝕜'}
(v : 𝕜') :
theorem
has_deriv_within_at.const_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{d : 𝕜 → 𝔸}
{d' : 𝔸}
(c : 𝔸)
(hd : has_deriv_within_at d d' s x) :
has_deriv_within_at (λ (y : 𝕜), c * d y) (c * d') s x
theorem
has_deriv_at.const_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{d : 𝕜 → 𝔸}
{d' : 𝔸}
(c : 𝔸)
(hd : has_deriv_at d d' x) :
has_deriv_at (λ (y : 𝕜), c * d y) (c * d') x
theorem
has_strict_deriv_at.const_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{d : 𝕜 → 𝔸}
{d' : 𝔸}
(c : 𝔸)
(hd : has_strict_deriv_at d d' x) :
has_strict_deriv_at (λ (y : 𝕜), c * d y) (c * d') x
theorem
deriv_within_const_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{d : 𝕜 → 𝔸}
(hxs : unique_diff_within_at 𝕜 s x)
(c : 𝔸)
(hd : differentiable_within_at 𝕜 d s x) :
deriv_within (λ (y : 𝕜), c * d y) s x = c * deriv_within d s x
theorem
deriv_const_mul
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝔸 : Type u_2}
[normed_ring 𝔸]
[normed_algebra 𝕜 𝔸]
{d : 𝕜 → 𝔸}
(c : 𝔸)
(hd : differentiable_at 𝕜 d x) :
theorem
deriv_const_mul_field
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜') :
@[simp]
theorem
deriv_const_mul_field'
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{𝕜' : Type u_1}
[normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜') :
theorem
has_deriv_at.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_at c c' x)
(d : 𝕜') :
has_deriv_at (λ (x : 𝕜), c x / d) (c' / d) x
theorem
has_deriv_within_at.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_deriv_within_at c c' s x)
(d : 𝕜') :
has_deriv_within_at (λ (x : 𝕜), c x / d) (c' / d) s x
theorem
has_strict_deriv_at.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
{c' : 𝕜'}
(hc : has_strict_deriv_at c c' x)
(d : 𝕜') :
has_strict_deriv_at (λ (x : 𝕜), c x / d) (c' / d) x
theorem
differentiable_within_at.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(hc : differentiable_within_at 𝕜 c s x)
(d : 𝕜') :
differentiable_within_at 𝕜 (λ (x : 𝕜), c x / d) s x
@[simp]
theorem
differentiable_at.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(hc : differentiable_at 𝕜 c x)
(d : 𝕜') :
differentiable_at 𝕜 (λ (x : 𝕜), c x / d) x
theorem
differentiable_on.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(hc : differentiable_on 𝕜 c s)
(d : 𝕜') :
differentiable_on 𝕜 (λ (x : 𝕜), c x / d) s
@[simp]
theorem
differentiable.div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(hc : differentiable 𝕜 c)
(d : 𝕜') :
differentiable 𝕜 (λ (x : 𝕜), c x / d)
theorem
deriv_within_div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(hc : differentiable_within_at 𝕜 c s x)
(d : 𝕜')
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (x : 𝕜), c x / d) s x = deriv_within c s x / d
@[simp]
theorem
deriv_div_const
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{x : 𝕜}
{𝕜' : Type u_1}
[nontrivially_normed_field 𝕜']
[normed_algebra 𝕜 𝕜']
{c : 𝕜 → 𝕜'}
(d : 𝕜') :
Derivative of the pointwise composition/application of continuous linear maps #
theorem
has_strict_deriv_at.clm_comp
{𝕜 : 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]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{d : 𝕜 → (E →L[𝕜] F)}
{d' : E →L[𝕜] F}
(hc : has_strict_deriv_at c c' x)
(hd : has_strict_deriv_at d d' x) :
has_strict_deriv_at (λ (y : 𝕜), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem
has_deriv_within_at.clm_comp
{𝕜 : 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]
{x : 𝕜}
{s : set 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{d : 𝕜 → (E →L[𝕜] F)}
{d' : E →L[𝕜] F}
(hc : has_deriv_within_at c c' s x)
(hd : has_deriv_within_at d d' s x) :
has_deriv_within_at (λ (y : 𝕜), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x
theorem
has_deriv_at.clm_comp
{𝕜 : 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]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{d : 𝕜 → (E →L[𝕜] F)}
{d' : E →L[𝕜] F}
(hc : has_deriv_at c c' x)
(hd : has_deriv_at d d' x) :
has_deriv_at (λ (y : 𝕜), (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem
deriv_within_clm_comp
{𝕜 : 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]
{x : 𝕜}
{s : set 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{d : 𝕜 → (E →L[𝕜] F)}
(hc : differentiable_within_at 𝕜 c s x)
(hd : differentiable_within_at 𝕜 d s x)
(hxs : unique_diff_within_at 𝕜 s x) :
deriv_within (λ (y : 𝕜), (c y).comp (d y)) s x = (deriv_within c s x).comp (d x) + (c x).comp (deriv_within d s x)
theorem
deriv_clm_comp
{𝕜 : 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]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{d : 𝕜 → (E →L[𝕜] F)}
(hc : differentiable_at 𝕜 c x)
(hd : differentiable_at 𝕜 d x) :
theorem
has_strict_deriv_at.clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{u : 𝕜 → F}
{u' : F}
(hc : has_strict_deriv_at c c' x)
(hu : has_strict_deriv_at u u' x) :
has_strict_deriv_at (λ (y : 𝕜), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') x
theorem
has_deriv_within_at.clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{u : 𝕜 → F}
{u' : F}
(hc : has_deriv_within_at c c' s x)
(hu : has_deriv_within_at u u' s x) :
has_deriv_within_at (λ (y : 𝕜), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') s x
theorem
has_deriv_at.clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{c' : F →L[𝕜] G}
{u : 𝕜 → F}
{u' : F}
(hc : has_deriv_at c c' x)
(hu : has_deriv_at u u' x) :
has_deriv_at (λ (y : 𝕜), ⇑(c y) (u y)) (⇑c' (u x) + ⇑(c x) u') x
theorem
deriv_within_clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{s : set 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{u : 𝕜 → F}
(hxs : unique_diff_within_at 𝕜 s x)
(hc : differentiable_within_at 𝕜 c s x)
(hu : differentiable_within_at 𝕜 u s x) :
deriv_within (λ (y : 𝕜), ⇑(c y) (u y)) s x = ⇑(deriv_within c s x) (u x) + ⇑(c x) (deriv_within u s x)
theorem
deriv_clm_apply
{𝕜 : Type u}
[nontrivially_normed_field 𝕜]
{F : Type v}
[normed_add_comm_group F]
[normed_space 𝕜 F]
{x : 𝕜}
{G : Type u_1}
[normed_add_comm_group G]
[normed_space 𝕜 G]
{c : 𝕜 → (F →L[𝕜] G)}
{u : 𝕜 → F}
(hc : differentiable_at 𝕜 c x)
(hu : differentiable_at 𝕜 u x) :