Documentation

Mathlib.Analysis.Calculus.Deriv.Mul

Derivative of f x * g x #

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 bilinear maps #

theorem ContinuousLinearMap.hasDerivWithinAt_of_bilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : 𝕜} {s : Set 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜E} {v : 𝕜F} {u' : E} {v' : F} (hu : HasDerivWithinAt u u' s x) (hv : HasDerivWithinAt v v' s x) :
HasDerivWithinAt (fun (x : 𝕜) => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x
theorem ContinuousLinearMap.hasDerivAt_of_bilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜E} {v : 𝕜F} {u' : E} {v' : F} (hu : HasDerivAt u u' x) (hv : HasDerivAt v v' x) :
HasDerivAt (fun (x : 𝕜) => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
theorem ContinuousLinearMap.hasStrictDerivAt_of_bilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜E} {v : 𝕜F} {u' : E} {v' : F} (hu : HasStrictDerivAt u u' x) (hv : HasStrictDerivAt v v' x) :
HasStrictDerivAt (fun (x : 𝕜) => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
theorem ContinuousLinearMap.derivWithin_of_bilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : 𝕜} {s : Set 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜E} {v : 𝕜F} (hxs : UniqueDiffWithinAt 𝕜 s x) (hu : DifferentiableWithinAt 𝕜 u s x) (hv : DifferentiableWithinAt 𝕜 v s x) :
derivWithin (fun (y : 𝕜) => (B (u y)) (v y)) s x = (B (u x)) (derivWithin v s x) + (B (derivWithin u s x)) (v x)
theorem ContinuousLinearMap.deriv_of_bilinear {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_1} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜E} {v : 𝕜F} (hu : DifferentiableAt 𝕜 u x) (hv : DifferentiableAt 𝕜 v x) :
deriv (fun (y : 𝕜) => (B (u y)) (v y)) x = (B (u x)) (deriv v x) + (B (deriv u x)) (v x)

Derivative of the multiplication of a scalar function and a vector function #

theorem HasDerivWithinAt.smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c y f y) (c x f' + c' f x) s x
theorem HasDerivAt.smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivAt c c' x) (hf : HasDerivAt f f' x) :
HasDerivAt (fun (y : 𝕜) => c y f y) (c x f' + c' f x) x
theorem HasStrictDerivAt.smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasStrictDerivAt c c' x) (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (y : 𝕜) => c y f y) (c x f' + c' f x) x
theorem derivWithin_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :
derivWithin (fun (y : 𝕜) => c y f y) s x = c x derivWithin f s x + derivWithin c s x f x
theorem deriv_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :
deriv (fun (y : 𝕜) => c y f y) x = c x deriv f x + deriv c x f x
theorem HasStrictDerivAt.smul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasStrictDerivAt c c' x) (f : F) :
HasStrictDerivAt (fun (y : 𝕜) => c y f) (c' f) x
theorem HasDerivWithinAt.smul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (f : F) :
HasDerivWithinAt (fun (y : 𝕜) => c y f) (c' f) s x
theorem HasDerivAt.smul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivAt c c' x) (f : F) :
HasDerivAt (fun (y : 𝕜) => c y f) (c' f) x
theorem derivWithin_smul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :
derivWithin (fun (y : 𝕜) => c y f) s x = derivWithin c s x f
theorem deriv_smul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜𝕜'} (hc : DifferentiableAt 𝕜 c x) (f : F) :
deriv (fun (y : 𝕜) => c y f) x = deriv c x f
theorem HasStrictDerivAt.const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : HasStrictDerivAt f f' x) :
HasStrictDerivAt (fun (y : 𝕜) => c f y) (c f') x
theorem HasDerivAtFilter.const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {L : Filter 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : HasDerivAtFilter f f' x L) :
HasDerivAtFilter (fun (y : 𝕜) => c f y) (c f') x L
theorem HasDerivWithinAt.const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : HasDerivWithinAt f f' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c f y) (c f') s x
theorem HasDerivAt.const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {f' : F} {x : 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : HasDerivAt f f' x) :
HasDerivAt (fun (y : 𝕜) => c f y) (c f') x
theorem derivWithin_const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (hxs : UniqueDiffWithinAt 𝕜 s x) (c : R) (hf : DifferentiableWithinAt 𝕜 f s x) :
derivWithin (fun (y : 𝕜) => c f y) s x = c derivWithin f s x
theorem deriv_const_smul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {R : Type u_2} [Semiring R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) (hf : DifferentiableAt 𝕜 f x) :
deriv (fun (y : 𝕜) => c f y) x = c deriv f x
theorem deriv_const_smul' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜F} {x : 𝕜} {R : Type u_3} [Field R] [Module R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R) :
deriv (fun (y : 𝕜) => c f y) x = c deriv f x

A variant of deriv_const_smul without differentiability assumption when the scalar multiplication is by field elements.

Derivative of the multiplication of two functions #

theorem HasDerivWithinAt.mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {d : 𝕜𝔸} {c' : 𝔸} {d' : 𝔸} (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c y * d y) (c' * d x + c x * d') s x
theorem HasDerivAt.mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {d : 𝕜𝔸} {c' : 𝔸} {d' : 𝔸} (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
HasDerivAt (fun (y : 𝕜) => c y * d y) (c' * d x + c x * d') x
theorem HasStrictDerivAt.mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {d : 𝕜𝔸} {c' : 𝔸} {d' : 𝔸} (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) :
HasStrictDerivAt (fun (y : 𝕜) => c y * d y) (c' * d x + c x * d') x
theorem derivWithin_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {d : 𝕜𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :
derivWithin (fun (y : 𝕜) => c y * d y) s x = derivWithin c s x * d x + c x * derivWithin d s x
@[simp]
theorem deriv_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {d : 𝕜𝔸} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
deriv (fun (y : 𝕜) => c y * d y) x = deriv c x * d x + c x * deriv d x
theorem HasDerivWithinAt.mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {c' : 𝔸} (hc : HasDerivWithinAt c c' s x) (d : 𝔸) :
HasDerivWithinAt (fun (y : 𝕜) => c y * d) (c' * d) s x
theorem HasDerivAt.mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {c' : 𝔸} (hc : HasDerivAt c c' x) (d : 𝔸) :
HasDerivAt (fun (y : 𝕜) => c y * d) (c' * d) x
theorem hasDerivAt_mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜) :
HasDerivAt (fun (x : 𝕜) => x * c) c x
theorem HasStrictDerivAt.mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} {c' : 𝔸} (hc : HasStrictDerivAt c c' x) (d : 𝔸) :
HasStrictDerivAt (fun (y : 𝕜) => c y * d) (c' * d) x
theorem derivWithin_mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸) :
derivWithin (fun (y : 𝕜) => c y * d) s x = derivWithin c s x * d
theorem deriv_mul_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {c : 𝕜𝔸} (hc : DifferentiableAt 𝕜 c x) (d : 𝔸) :
deriv (fun (y : 𝕜) => c y * d) x = deriv c x * d
theorem deriv_mul_const_field {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {u : 𝕜𝕜'} (v : 𝕜') :
deriv (fun (y : 𝕜) => u y * v) x = deriv u x * v
@[simp]
theorem deriv_mul_const_field' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {u : 𝕜𝕜'} (v : 𝕜') :
(deriv fun (x : 𝕜) => u x * v) = fun (x : 𝕜) => deriv u x * v
theorem HasDerivWithinAt.const_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {d : 𝕜𝔸} {d' : 𝔸} (c : 𝔸) (hd : HasDerivWithinAt d d' s x) :
HasDerivWithinAt (fun (y : 𝕜) => c * d y) (c * d') s x
theorem HasDerivAt.const_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {d : 𝕜𝔸} {d' : 𝔸} (c : 𝔸) (hd : HasDerivAt d d' x) :
HasDerivAt (fun (y : 𝕜) => c * d y) (c * d') x
theorem HasStrictDerivAt.const_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {d : 𝕜𝔸} {d' : 𝔸} (c : 𝔸) (hd : HasStrictDerivAt d d' x) :
HasStrictDerivAt (fun (y : 𝕜) => c * d y) (c * d') x
theorem derivWithin_const_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {d : 𝕜𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (c : 𝔸) (hd : DifferentiableWithinAt 𝕜 d s x) :
derivWithin (fun (y : 𝕜) => c * d y) s x = c * derivWithin d s x
theorem deriv_const_mul {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {d : 𝕜𝔸} (c : 𝔸) (hd : DifferentiableAt 𝕜 d x) :
deriv (fun (y : 𝕜) => c * d y) x = c * deriv d x
theorem deriv_const_mul_field {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {v : 𝕜𝕜'} (u : 𝕜') :
deriv (fun (y : 𝕜) => u * v y) x = u * deriv v x
@[simp]
theorem deriv_const_mul_field' {𝕜 : Type u} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {v : 𝕜𝕜'} (u : 𝕜') :
(deriv fun (x : 𝕜) => u * v x) = fun (x : 𝕜) => u * deriv v x
theorem HasDerivAt.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [DecidableEq ι] {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} {f' : ι𝔸'} (hf : iu, HasDerivAt (f i) (f' i) x) :
HasDerivAt (fun (x : 𝕜) => iu, f i x) (∑ iu, (∏ ju.erase i, f j x) f' i) x
theorem HasDerivWithinAt.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [DecidableEq ι] {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} {f' : ι𝔸'} (hf : iu, HasDerivWithinAt (f i) (f' i) s x) :
HasDerivWithinAt (fun (x : 𝕜) => iu, f i x) (∑ iu, (∏ ju.erase i, f j x) f' i) s x
theorem HasStrictDerivAt.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [DecidableEq ι] {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} {f' : ι𝔸'} (hf : iu, HasStrictDerivAt (f i) (f' i) x) :
HasStrictDerivAt (fun (x : 𝕜) => iu, f i x) (∑ iu, (∏ ju.erase i, f j x) f' i) x
theorem deriv_finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [DecidableEq ι] {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hf : iu, DifferentiableAt 𝕜 (f i) x) :
deriv (fun (x : 𝕜) => iu, f i x) x = iu, (∏ ju.erase i, f j x) deriv (f i) x
theorem derivWithin_finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [DecidableEq ι] {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : iu, DifferentiableWithinAt 𝕜 (f i) s x) :
derivWithin (fun (x : 𝕜) => iu, f i x) s x = iu, (∏ ju.erase i, f j x) derivWithin (f i) s x
theorem DifferentiableAt.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hd : iu, DifferentiableAt 𝕜 (f i) x) :
DifferentiableAt 𝕜 (fun (x : 𝕜) => iu, f i x) x
theorem DifferentiableWithinAt.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hd : iu, DifferentiableWithinAt 𝕜 (f i) s x) :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => iu, f i x) s x
theorem DifferentiableOn.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hd : iu, DifferentiableOn 𝕜 (f i) s) :
DifferentiableOn 𝕜 (fun (x : 𝕜) => iu, f i x) s
theorem Differentiable.finset_prod {𝕜 : Type u} [NontriviallyNormedField 𝕜] {ι : Type u_2} {𝔸' : Type u_3} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι𝕜𝔸'} (hd : iu, Differentiable 𝕜 (f i)) :
Differentiable 𝕜 fun (x : 𝕜) => iu, f i x
theorem HasDerivAt.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivAt c c' x) (d : 𝕜') :
HasDerivAt (fun (x : 𝕜) => c x / d) (c' / d) x
theorem HasDerivWithinAt.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasDerivWithinAt c c' s x) (d : 𝕜') :
HasDerivWithinAt (fun (x : 𝕜) => c x / d) (c' / d) s x
theorem HasStrictDerivAt.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} {c' : 𝕜'} (hc : HasStrictDerivAt c c' x) (d : 𝕜') :
HasStrictDerivAt (fun (x : 𝕜) => c x / d) (c' / d) x
theorem DifferentiableWithinAt.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝕜') :
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => c x / d) s x
@[simp]
theorem DifferentiableAt.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (hc : DifferentiableAt 𝕜 c x) (d : 𝕜') :
DifferentiableAt 𝕜 (fun (x : 𝕜) => c x / d) x
theorem DifferentiableOn.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (hc : DifferentiableOn 𝕜 c s) (d : 𝕜') :
DifferentiableOn 𝕜 (fun (x : 𝕜) => c x / d) s
@[simp]
theorem Differentiable.div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (hc : Differentiable 𝕜 c) (d : 𝕜') :
Differentiable 𝕜 fun (x : 𝕜) => c x / d
theorem derivWithin_div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝕜') (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (x : 𝕜) => c x / d) s x = derivWithin c s x / d
@[simp]
theorem deriv_div_const {𝕜 : Type u} [NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] {c : 𝕜𝕜'} (d : 𝕜') :
deriv (fun (x : 𝕜) => c x / d) x = deriv c x / d

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

theorem HasStrictDerivAt.clm_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {d : 𝕜E →L[𝕜] F} {d' : E →L[𝕜] F} (hc : HasStrictDerivAt c c' x) (hd : HasStrictDerivAt d d' x) :
HasStrictDerivAt (fun (y : 𝕜) => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem HasDerivWithinAt.clm_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {d : 𝕜E →L[𝕜] F} {d' : E →L[𝕜] F} (hc : HasDerivWithinAt c c' s x) (hd : HasDerivWithinAt d d' s x) :
HasDerivWithinAt (fun (y : 𝕜) => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') s x
theorem HasDerivAt.clm_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {d : 𝕜E →L[𝕜] F} {d' : E →L[𝕜] F} (hc : HasDerivAt c c' x) (hd : HasDerivAt d d' x) :
HasDerivAt (fun (y : 𝕜) => (c y).comp (d y)) (c'.comp (d x) + (c x).comp d') x
theorem derivWithin_clm_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {d : 𝕜E →L[𝕜] F} (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) (hxs : UniqueDiffWithinAt 𝕜 s x) :
derivWithin (fun (y : 𝕜) => (c y).comp (d y)) s x = (derivWithin c s x).comp (d x) + (c x).comp (derivWithin d s x)
theorem deriv_clm_comp {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {E : Type w} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {d : 𝕜E →L[𝕜] F} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :
deriv (fun (y : 𝕜) => (c y).comp (d y)) x = (deriv c x).comp (d x) + (c x).comp (deriv d x)
theorem HasStrictDerivAt.clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜F} {u' : F} (hc : HasStrictDerivAt c c' x) (hu : HasStrictDerivAt u u' x) :
HasStrictDerivAt (fun (y : 𝕜) => (c y) (u y)) (c' (u x) + (c x) u') x
theorem HasDerivWithinAt.clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜F} {u' : F} (hc : HasDerivWithinAt c c' s x) (hu : HasDerivWithinAt u u' s x) :
HasDerivWithinAt (fun (y : 𝕜) => (c y) (u y)) (c' (u x) + (c x) u') s x
theorem HasDerivAt.clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜F} {u' : F} (hc : HasDerivAt c c' x) (hu : HasDerivAt u u' x) :
HasDerivAt (fun (y : 𝕜) => (c y) (u y)) (c' (u x) + (c x) u') x
theorem derivWithin_clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {u : 𝕜F} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :
derivWithin (fun (y : 𝕜) => (c y) (u y)) s x = (derivWithin c s x) (u x) + (c x) (derivWithin u s x)
theorem deriv_clm_apply {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : 𝕜} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {c : 𝕜F →L[𝕜] G} {u : 𝕜F} (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :
deriv (fun (y : 𝕜) => (c y) (u y)) x = (deriv c x) (u x) + (c x) (deriv u x)