mathlib3 documentation

analysis.calculus.deriv.mul

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) :
deriv (λ (y : 𝕜), c y f y) x = c x deriv f x + deriv c x 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) :
deriv (λ (y : 𝕜), c y f) x = deriv c x 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) :
deriv (λ (y : 𝕜), c f y) x = c deriv 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) :
deriv (λ (y : 𝕜), c y * d y) x = deriv c x * d x + c x * deriv 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 : 𝔸) :
deriv (λ (y : 𝕜), c y * d) x = deriv c x * d
theorem deriv_mul_const_field {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {𝕜' : Type u_1} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {u : 𝕜 𝕜'} (v : 𝕜') :
deriv (λ (y : 𝕜), u y * v) x = deriv u x * v
@[simp]
theorem deriv_mul_const_field' {𝕜 : Type u} [nontrivially_normed_field 𝕜] {𝕜' : Type u_1} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {u : 𝕜 𝕜'} (v : 𝕜') :
deriv (λ (x : 𝕜), u x * v) = λ (x : 𝕜), deriv u x * 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) :
deriv (λ (y : 𝕜), c * d y) x = c * deriv d x
theorem deriv_const_mul_field {𝕜 : Type u} [nontrivially_normed_field 𝕜] {x : 𝕜} {𝕜' : Type u_1} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {v : 𝕜 𝕜'} (u : 𝕜') :
deriv (λ (y : 𝕜), u * v y) x = u * deriv v x
@[simp]
theorem deriv_const_mul_field' {𝕜 : Type u} [nontrivially_normed_field 𝕜] {𝕜' : Type u_1} [normed_field 𝕜'] [normed_algebra 𝕜 𝕜'] {v : 𝕜 𝕜'} (u : 𝕜') :
deriv (λ (x : 𝕜), u * v x) = λ (x : 𝕜), u * deriv v x
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 : 𝕜') :
deriv (λ (x : 𝕜), c x / d) x = deriv c x / 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) :
deriv (λ (y : 𝕜), (c y).comp (d y)) x = (deriv c x).comp (d x) + (c x).comp (deriv 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) :
deriv (λ (y : 𝕜), (c y) (u y)) x = (deriv c x) (u x) + (c x) (deriv u x)