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)
:
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)
:
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)
:
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)
:
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)
:
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)
:
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 : 𝔸)
:
theorem
deriv_mul_const_field
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{u : 𝕜 → 𝕜'}
(v : 𝕜')
:
@[simp]
theorem
deriv_mul_const_field'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{u : 𝕜 → 𝕜'}
(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)
:
theorem
deriv_const_mul_field
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜')
:
@[simp]
theorem
deriv_const_mul_field'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜')
:
theorem
HasDerivAt.finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{ι : Type u_2}
[DecidableEq ι]
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
{f' : ι → 𝔸'}
(hf : ∀ i ∈ u, HasDerivAt (f i) (f' i) x)
:
HasDerivAt (fun (x : 𝕜) => Finset.prod u fun (i : ι) => f i x)
(Finset.sum u fun (i : ι) => (Finset.prod (Finset.erase u i) fun (j : ι) => 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 : ∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x)
:
HasDerivWithinAt (fun (x : 𝕜) => Finset.prod u fun (i : ι) => f i x)
(Finset.sum u fun (i : ι) => (Finset.prod (Finset.erase u i) fun (j : ι) => 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 : ∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x)
:
HasStrictDerivAt (fun (x : 𝕜) => Finset.prod u fun (i : ι) => f i x)
(Finset.sum u fun (i : ι) => (Finset.prod (Finset.erase u i) fun (j : ι) => 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 : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x)
:
deriv (fun (x : 𝕜) => Finset.prod u fun (i : ι) => f i x) x = Finset.sum u fun (i : ι) => (Finset.prod (Finset.erase u i) fun (j : ι) => 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 : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x)
:
derivWithin (fun (x : 𝕜) => Finset.prod u fun (i : ι) => f i x) s x = Finset.sum u fun (i : ι) => (Finset.prod (Finset.erase u i) fun (j : ι) => f j x) • derivWithin (f i) s 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 : 𝕜')
:
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 : 𝕜) => ContinuousLinearMap.comp (c y) (d y))
(ContinuousLinearMap.comp c' (d x) + ContinuousLinearMap.comp (c x) 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 : 𝕜) => ContinuousLinearMap.comp (c y) (d y))
(ContinuousLinearMap.comp c' (d x) + ContinuousLinearMap.comp (c x) 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 : 𝕜) => ContinuousLinearMap.comp (c y) (d y))
(ContinuousLinearMap.comp c' (d x) + ContinuousLinearMap.comp (c x) 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 : 𝕜) => ContinuousLinearMap.comp (c y) (d y)) s x = ContinuousLinearMap.comp (derivWithin c s x) (d x) + ContinuousLinearMap.comp (c x) (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 : 𝕜) => ContinuousLinearMap.comp (c y) (d y)) x = ContinuousLinearMap.comp (deriv c x) (d x) + ContinuousLinearMap.comp (c x) (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)
: