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
Mathlib/Analysis/Calculus/Deriv/Basic.lean.
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}
(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 (c • f) (c x • f' + c' • f x) s x
theorem
HasDerivWithinAt.fun_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 (i : 𝕜) => c i • f i) (c x • f' + c' • f x) s x
Eta-expanded form of HasDerivWithinAt.smul
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 (c • f) (c x • f' + c' • f x) x
theorem
HasDerivAt.fun_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 (i : 𝕜) => c i • f i) (c x • f' + c' • f x) x
Eta-expanded form of HasDerivAt.smul
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 (c • f) (c x • f' + c' • f x) x
theorem
HasStrictDerivAt.fun_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 (i : 𝕜) => c i • f i) (c x • f' + c' • f x) x
Eta-expanded form of HasStrictDerivAt.smul
theorem
derivWithin_fun_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 : 𝕜 → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s 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 : 𝕜 → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
theorem
deriv_fun_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
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 : 𝕜 → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(f : 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 (c • f) (c • f') x
theorem
HasStrictDerivAt.fun_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 (i : 𝕜) => c • f i) (c • f') x
Eta-expanded form of HasStrictDerivAt.const_smul
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 (c • f) (c • f') x L
theorem
HasDerivAtFilter.fun_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 (i : 𝕜) => c • f i) (c • f') x L
Eta-expanded form of HasDerivAtFilter.const_smul
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 (c • f) (c • f') s x
theorem
HasDerivWithinAt.fun_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 (i : 𝕜) => c • f i) (c • f') s x
Eta-expanded form of HasDerivWithinAt.const_smul
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 (c • f) (c • f') x
theorem
HasDerivAt.fun_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 (i : 𝕜) => c • f i) (c • f') x
Eta-expanded form of HasDerivAt.const_smul
theorem
derivWithin_fun_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]
(c : R)
(hf : DifferentiableWithinAt 𝕜 f s 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]
(c : R)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
theorem
derivWithin_fun_const_smul'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set 𝕜}
{f : 𝕜 → F}
{x : 𝕜}
{R : Type u_3}
[Field R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
(c : R)
:
A variant of derivWithin_fun_const_smul without differentiability assumption when the scalar
multiplication is by field elements.
theorem
derivWithin_const_smul'
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set 𝕜}
{f : 𝕜 → F}
{x : 𝕜}
{R : Type u_3}
[Field R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
(c : R)
:
A variant of derivWithin_const_smul without differentiability assumption when the scalar
multiplication is by field elements.
theorem
deriv_fun_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_2}
[Semiring R]
[Module R F]
[SMulCommClass 𝕜 R F]
[ContinuousConstSMul R F]
(c : R)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
deriv_fun_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.
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 (c * d) (c' * d x + c x * d') s x
theorem
HasDerivWithinAt.fun_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 (i : 𝕜) => c i * d i) (c' * d x + c x * d') s x
Eta-expanded form of HasDerivWithinAt.mul
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 (c * d) (c' * d x + c x * d') x
theorem
HasDerivAt.fun_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 (i : 𝕜) => c i * d i) (c' * d x + c x * d') x
Eta-expanded form of HasDerivAt.mul
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 (c * d) (c' * d x + c x * d') x
theorem
HasStrictDerivAt.fun_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 (i : 𝕜) => c i * d i) (c' * d x + c x * d') x
Eta-expanded form of HasStrictDerivAt.mul
theorem
derivWithin_fun_mul
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x)
:
theorem
derivWithin_mul
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x)
:
@[simp]
theorem
deriv_fun_mul
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{𝔸 : Type u_3}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{c d : 𝕜 → 𝔸}
(hc : DifferentiableAt 𝕜 c x)
(hd : DifferentiableAt 𝕜 d 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 : 𝕜 → 𝔸}
(hc : DifferentiableWithinAt 𝕜 c s x)
(d : 𝔸)
:
theorem
derivWithin_mul_const_field
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜')
:
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
hasDerivAt_const_mul
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
(c : 𝕜)
:
HasDerivAt (fun (y : 𝕜) => c * y) c 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 : 𝕜 → 𝔸}
(c : 𝔸)
(hd : DifferentiableWithinAt 𝕜 d s x)
:
theorem
derivWithin_const_mul_field
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{𝕜' : Type u_2}
[NormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
{v : 𝕜 → 𝕜'}
(u : 𝕜')
:
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.fun_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 : 𝕜) => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
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 (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
theorem
HasDerivWithinAt.fun_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 : 𝕜) => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s 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 (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
theorem
HasStrictDerivAt.fun_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 : 𝕜) => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) 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 (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
theorem
deriv_fun_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)
:
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)
:
theorem
derivWithin_fun_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{ι : Type u_2}
[DecidableEq ι]
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x)
:
derivWithin (fun (x : 𝕜) => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
theorem
derivWithin_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{ι : Type u_2}
[DecidableEq ι]
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x)
:
theorem
DifferentiableAt.fun_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x)
:
DifferentiableAt 𝕜 (fun (x : 𝕜) => ∏ i ∈ u, f i x) x
theorem
DifferentiableAt.finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableAt 𝕜 (f i) x)
:
DifferentiableAt 𝕜 (∏ i ∈ u, f i) x
theorem
DifferentiableWithinAt.fun_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x)
:
DifferentiableWithinAt 𝕜 (fun (x : 𝕜) => ∏ i ∈ u, f i x) s x
theorem
DifferentiableWithinAt.finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{x : 𝕜}
{s : Set 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x)
:
DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i) s x
theorem
DifferentiableOn.fun_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableOn 𝕜 (f i) s)
:
DifferentiableOn 𝕜 (fun (x : 𝕜) => ∏ i ∈ u, f i x) s
theorem
DifferentiableOn.finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{s : Set 𝕜}
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, DifferentiableOn 𝕜 (f i) s)
:
DifferentiableOn 𝕜 (∏ i ∈ u, f i) s
theorem
Differentiable.fun_finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, Differentiable 𝕜 (f i))
:
Differentiable 𝕜 fun (x : 𝕜) => ∏ i ∈ u, f i x
theorem
Differentiable.finset_prod
{𝕜 : Type u}
[NontriviallyNormedField 𝕜]
{ι : Type u_2}
{𝔸' : Type u_3}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{f : ι → 𝕜 → 𝔸'}
(hd : ∀ i ∈ u, Differentiable 𝕜 (f i))
:
Differentiable 𝕜 (∏ i ∈ u, f i)
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 : 𝕜')
:
@[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 : 𝕜) => (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)
:
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)
:
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}
(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)
: