# mathlib3documentation

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} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : s x) (hf : 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} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : c' x) (hf : 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} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : x) (hf : x) :
has_strict_deriv_at (λ (y : 𝕜), c y f y) (c x f' + c' f x) x
theorem deriv_within_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} (hxs : x) (hc : x) (hf : x) :
deriv_within (λ (y : 𝕜), c y f y) s x = c x s x + s x f x
theorem deriv_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} (hc : x) (hf : x) :
deriv (λ (y : 𝕜), c y f y) x = c x x + x f x
theorem has_strict_deriv_at.smul_const {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : x) (f : F) :
has_strict_deriv_at (λ (y : 𝕜), c y f) (c' f) x
theorem has_deriv_within_at.smul_const {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : s x) (f : F) :
has_deriv_within_at (λ (y : 𝕜), c y f) (c' f) s x
theorem has_deriv_at.smul_const {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : c' x) (f : F) :
has_deriv_at (λ (y : 𝕜), c y f) (c' f) x
theorem deriv_within_smul_const {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} (hxs : x) (hc : x) (f : F) :
deriv_within (λ (y : 𝕜), c y f) s x = s x f
theorem deriv_smul_const {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] [ F] [ 𝕜' F] {c : 𝕜 𝕜'} (hc : x) (f : F) :
deriv (λ (y : 𝕜), c y f) x = x f
theorem has_strict_deriv_at.const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (c : R) (hf : x) :
has_strict_deriv_at (λ (y : 𝕜), c f y) (c f') x
theorem has_deriv_at_filter.const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {L : filter 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (c : R) (hf : x L) :
has_deriv_at_filter (λ (y : 𝕜), c f y) (c f') x L
theorem has_deriv_within_at.const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {s : set 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (c : R) (hf : s x) :
has_deriv_within_at (λ (y : 𝕜), c f y) (c f') s x
theorem has_deriv_at.const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {f' : F} {x : 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (c : R) (hf : f' x) :
has_deriv_at (λ (y : 𝕜), c f y) (c f') x
theorem deriv_within_const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {s : set 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (hxs : x) (c : R) (hf : x) :
deriv_within (λ (y : 𝕜), c f y) s x = c s x
theorem deriv_const_smul {𝕜 : Type u} {F : Type v} [ F] {f : 𝕜 F} {x : 𝕜} {R : Type u_1} [semiring R] [ F] [ F] (c : R) (hf : x) :
deriv (λ (y : 𝕜), c f y) x = c x

### Derivative of the multiplication of two functions #

theorem has_deriv_within_at.mul {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c d : 𝕜 𝔸} {c' d' : 𝔸} (hc : s x) (hd : 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} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c d : 𝕜 𝔸} {c' d' : 𝔸} (hc : c' x) (hd : 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} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c d : 𝕜 𝔸} {c' d' : 𝔸} (hc : x) (hd : x) :
has_strict_deriv_at (λ (y : 𝕜), c y * d y) (c' * d x + c x * d') x
theorem deriv_within_mul {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c d : 𝕜 𝔸} (hxs : x) (hc : x) (hd : x) :
deriv_within (λ (y : 𝕜), c y * d y) s x = s x * d x + c x * s x
@[simp]
theorem deriv_mul {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c d : 𝕜 𝔸} (hc : x) (hd : x) :
deriv (λ (y : 𝕜), c y * d y) x = x * d x + c x * x
theorem has_deriv_within_at.mul_const {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c : 𝕜 𝔸} {c' : 𝔸} (hc : s x) (d : 𝔸) :
has_deriv_within_at (λ (y : 𝕜), c y * d) (c' * d) s x
theorem has_deriv_at.mul_const {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c : 𝕜 𝔸} {c' : 𝔸} (hc : c' x) (d : 𝔸) :
has_deriv_at (λ (y : 𝕜), c y * d) (c' * d) x
theorem has_deriv_at_mul_const {𝕜 : Type u} {x : 𝕜} (c : 𝕜) :
has_deriv_at (λ (x : 𝕜), x * c) c x
theorem has_strict_deriv_at.mul_const {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c : 𝕜 𝔸} {c' : 𝔸} (hc : x) (d : 𝔸) :
has_strict_deriv_at (λ (y : 𝕜), c y * d) (c' * d) x
theorem deriv_within_mul_const {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c : 𝕜 𝔸} (hxs : x) (hc : x) (d : 𝔸) :
deriv_within (λ (y : 𝕜), c y * d) s x = s x * d
theorem deriv_mul_const {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {c : 𝕜 𝔸} (hc : x) (d : 𝔸) :
deriv (λ (y : 𝕜), c y * d) x = x * d
theorem deriv_mul_const_field {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [normed_field 𝕜'] [ 𝕜'] {u : 𝕜 𝕜'} (v : 𝕜') :
deriv (λ (y : 𝕜), u y * v) x = x * v
@[simp]
theorem deriv_mul_const_field' {𝕜 : Type u} {𝕜' : Type u_1} [normed_field 𝕜'] [ 𝕜'] {u : 𝕜 𝕜'} (v : 𝕜') :
deriv (λ (x : 𝕜), u x * v) = λ (x : 𝕜), x * v
theorem has_deriv_within_at.const_mul {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {d : 𝕜 𝔸} {d' : 𝔸} (c : 𝔸) (hd : s x) :
has_deriv_within_at (λ (y : 𝕜), c * d y) (c * d') s x
theorem has_deriv_at.const_mul {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {d : 𝕜 𝔸} {d' : 𝔸} (c : 𝔸) (hd : d' x) :
has_deriv_at (λ (y : 𝕜), c * d y) (c * d') x
theorem has_strict_deriv_at.const_mul {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {d : 𝕜 𝔸} {d' : 𝔸} (c : 𝔸) (hd : x) :
has_strict_deriv_at (λ (y : 𝕜), c * d y) (c * d') x
theorem deriv_within_const_mul {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {d : 𝕜 𝔸} (hxs : x) (c : 𝔸) (hd : x) :
deriv_within (λ (y : 𝕜), c * d y) s x = c * s x
theorem deriv_const_mul {𝕜 : Type u} {x : 𝕜} {𝔸 : Type u_2} [normed_ring 𝔸] [ 𝔸] {d : 𝕜 𝔸} (c : 𝔸) (hd : x) :
deriv (λ (y : 𝕜), c * d y) x = c * x
theorem deriv_const_mul_field {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [normed_field 𝕜'] [ 𝕜'] {v : 𝕜 𝕜'} (u : 𝕜') :
deriv (λ (y : 𝕜), u * v y) x = u * x
@[simp]
theorem deriv_const_mul_field' {𝕜 : Type u} {𝕜' : Type u_1} [normed_field 𝕜'] [ 𝕜'] {v : 𝕜 𝕜'} (u : 𝕜') :
deriv (λ (x : 𝕜), u * v x) = λ (x : 𝕜), u * x
theorem has_deriv_at.div_const {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : c' x) (d : 𝕜') :
has_deriv_at (λ (x : 𝕜), c x / d) (c' / d) x
theorem has_deriv_within_at.div_const {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : s x) (d : 𝕜') :
has_deriv_within_at (λ (x : 𝕜), c x / d) (c' / d) s x
theorem has_strict_deriv_at.div_const {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} {c' : 𝕜'} (hc : x) (d : 𝕜') :
has_strict_deriv_at (λ (x : 𝕜), c x / d) (c' / d) x
theorem differentiable_within_at.div_const {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (hc : x) (d : 𝕜') :
(λ (x : 𝕜), c x / d) s x
@[simp]
theorem differentiable_at.div_const {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (hc : x) (d : 𝕜') :
(λ (x : 𝕜), c x / d) x
theorem differentiable_on.div_const {𝕜 : Type u} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (hc : s) (d : 𝕜') :
(λ (x : 𝕜), c x / d) s
@[simp]
theorem differentiable.div_const {𝕜 : Type u} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (hc : c) (d : 𝕜') :
(λ (x : 𝕜), c x / d)
theorem deriv_within_div_const {𝕜 : Type u} {x : 𝕜} {s : set 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (hc : x) (d : 𝕜') (hxs : x) :
deriv_within (λ (x : 𝕜), c x / d) s x = s x / d
@[simp]
theorem deriv_div_const {𝕜 : Type u} {x : 𝕜} {𝕜' : Type u_1} [ 𝕜'] {c : 𝕜 𝕜'} (d : 𝕜') :
deriv (λ (x : 𝕜), c x / d) x = x / d

### Derivative of the pointwise composition/application of continuous linear maps #

theorem has_strict_deriv_at.clm_comp {𝕜 : Type u} {F : Type v} [ F] {E : Type w} [ E] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {d : 𝕜 (E →L[𝕜] F)} {d' : E →L[𝕜] F} (hc : x) (hd : 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} {F : Type v} [ F] {E : Type w} [ E] {x : 𝕜} {s : set 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {d : 𝕜 (E →L[𝕜] F)} {d' : E →L[𝕜] F} (hc : s x) (hd : 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} {F : Type v} [ F] {E : Type w} [ E] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {d : 𝕜 (E →L[𝕜] F)} {d' : E →L[𝕜] F} (hc : c' x) (hd : 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} {F : Type v} [ F] {E : Type w} [ E] {x : 𝕜} {s : set 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {d : 𝕜 (E →L[𝕜] F)} (hc : x) (hd : x) (hxs : x) :
deriv_within (λ (y : 𝕜), (c y).comp (d y)) s x = s x).comp (d x) + (c x).comp s x)
theorem deriv_clm_comp {𝕜 : Type u} {F : Type v} [ F] {E : Type w} [ E] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {d : 𝕜 (E →L[𝕜] F)} (hc : x) (hd : 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} {F : Type v} [ F] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {u : 𝕜 F} {u' : F} (hc : x) (hu : 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} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {u : 𝕜 F} {u' : F} (hc : s x) (hu : 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} {F : Type v} [ F] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {c' : F →L[𝕜] G} {u : 𝕜 F} {u' : F} (hc : c' x) (hu : u' x) :
has_deriv_at (λ (y : 𝕜), (c y) (u y)) (c' (u x) + (c x) u') x
theorem deriv_within_clm_apply {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {s : set 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {u : 𝕜 F} (hxs : x) (hc : x) (hu : x) :
deriv_within (λ (y : 𝕜), (c y) (u y)) s x = s x) (u x) + (c x) s x)
theorem deriv_clm_apply {𝕜 : Type u} {F : Type v} [ F] {x : 𝕜} {G : Type u_1} [ G] {c : 𝕜 (F →L[𝕜] G)} {u : 𝕜 F} (hc : x) (hu : x) :
deriv (λ (y : 𝕜), (c y) (u y)) x = (deriv c x) (u x) + (c x) (deriv u x)