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 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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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

Derivative of the multiplication of two functions #

theorem HasDerivWithinAt.mul {π•œ : Type u} [NontriviallyNormedField π•œ] {x : π•œ} {s : Set π•œ} {𝔸 : Type u_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_2} [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_1} [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_1} [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_2} [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_2} [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_2} [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_2} [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_2} [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_1} [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_1} [NormedField π•œ'] [NormedAlgebra π•œ π•œ'] {v : π•œ β†’ π•œ'} (u : π•œ') :
(deriv fun x => u * v x) = fun x => u * deriv v x
theorem HasDerivAt.div_const {π•œ : Type u} [NontriviallyNormedField π•œ] {x : π•œ} {π•œ' : Type u_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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_1} [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) :
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_1} [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) :
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_1} [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) :
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_1} [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) :
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_1} [NormedAddCommGroup G] [NormedSpace π•œ G] {c : π•œ β†’ F β†’L[π•œ] G} {d : π•œ β†’ E β†’L[π•œ] F} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
theorem HasStrictDerivAt.clm_apply {π•œ : Type u} [NontriviallyNormedField π•œ] {F : Type v} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : π•œ} {G : Type u_1} [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_1} [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_1} [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_1} [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_1} [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)