Multiplicative operations on derivatives #
For detailed documentation of the Fréchet derivative,
see the module docstring of Mathlib/Analysis/Calculus/FDeriv/Basic.lean.
This file contains the usual formulas (and existence assertions) for the derivative of
- multiplication of a function by a scalar function
- product of finitely many scalar functions
- taking the pointwise multiplicative inverse (i.e.
Inv.invorRing.inverse) of a function
Derivative of the product of a scalar-valued function and a vector-valued function #
If c is a differentiable scalar-valued function and f is a differentiable vector-valued
function, then fun x ↦ c x • f x is differentiable as well. Lemmas in this section works for
function c taking values in the base field, as well as in a normed algebra over the base
field: e.g., they work for c : E → ℂ and f : E → F provided that F is a complex
normed vector space.
theorem
HasStrictFDerivAt.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasStrictFDerivAt c c' x)
(hf : HasStrictFDerivAt f f' x)
:
HasStrictFDerivAt (fun (y : E) => c y • f y) (c x • f' + c'.smulRight (f x)) x
theorem
HasStrictFDerivAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasStrictFDerivAt c c' x)
(hf : HasStrictFDerivAt f f' x)
:
HasStrictFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x
theorem
HasFDerivWithinAt.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivWithinAt c c' s x)
(hf : HasFDerivWithinAt f f' s x)
:
HasFDerivWithinAt (fun (y : E) => c y • f y) (c x • f' + c'.smulRight (f x)) s x
theorem
HasFDerivWithinAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivWithinAt c c' s x)
(hf : HasFDerivWithinAt f f' s x)
:
HasFDerivWithinAt (c • f) (c x • f' + c'.smulRight (f x)) s x
theorem
HasFDerivAt.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivAt c c' x)
(hf : HasFDerivAt f f' x)
:
HasFDerivAt (fun (y : E) => c y • f y) (c x • f' + c'.smulRight (f x)) x
theorem
HasFDerivAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{f' : E →L[𝕜] F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivAt c c' x)
(hf : HasFDerivAt f f' x)
:
HasFDerivAt (c • f) (c x • f' + c'.smulRight (f x)) x
theorem
DifferentiableWithinAt.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
DifferentiableWithinAt 𝕜 (fun (y : E) => c y • f y) s x
theorem
DifferentiableWithinAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
DifferentiableWithinAt 𝕜 (c • f) s x
@[simp]
theorem
DifferentiableAt.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(hf : DifferentiableAt 𝕜 f x)
:
DifferentiableAt 𝕜 (fun (y : E) => c y • f y) x
@[simp]
theorem
DifferentiableAt.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(hf : DifferentiableAt 𝕜 f x)
:
DifferentiableAt 𝕜 (c • f) x
theorem
DifferentiableOn.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableOn 𝕜 c s)
(hf : DifferentiableOn 𝕜 f s)
:
DifferentiableOn 𝕜 (fun (y : E) => c y • f y) s
theorem
DifferentiableOn.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableOn 𝕜 c s)
(hf : DifferentiableOn 𝕜 f s)
:
DifferentiableOn 𝕜 (c • f) s
@[simp]
theorem
Differentiable.fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : Differentiable 𝕜 c)
(hf : Differentiable 𝕜 f)
:
Differentiable 𝕜 fun (y : E) => c y • f y
@[simp]
theorem
Differentiable.smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : Differentiable 𝕜 c)
(hf : Differentiable 𝕜 f)
:
Differentiable 𝕜 (c • f)
theorem
fderivWithin_fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
fderivWithin 𝕜 (fun (y : E) => c y • f y) s x = c x • fderivWithin 𝕜 f s x + (fderivWithin 𝕜 c s x).smulRight (f x)
theorem
fderivWithin_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(hf : DifferentiableWithinAt 𝕜 f s x)
:
theorem
fderiv_fun_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
fderiv_smul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(hf : DifferentiableAt 𝕜 f x)
:
theorem
HasStrictFDerivAt.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasStrictFDerivAt c c' x)
(f : F)
:
HasStrictFDerivAt (fun (y : E) => c y • f) (c'.smulRight f) x
theorem
HasFDerivWithinAt.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivWithinAt c c' s x)
(f : F)
:
HasFDerivWithinAt (fun (y : E) => c y • f) (c'.smulRight f) s x
theorem
HasFDerivAt.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
{c' : E →L[𝕜] 𝕜'}
(hc : HasFDerivAt c c' x)
(f : F)
:
HasFDerivAt (fun (y : E) => c y • f) (c'.smulRight f) x
theorem
DifferentiableWithinAt.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableWithinAt 𝕜 c s x)
(f : F)
:
DifferentiableWithinAt 𝕜 (fun (y : E) => c y • f) s x
theorem
DifferentiableAt.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(f : F)
:
DifferentiableAt 𝕜 (fun (y : E) => c y • f) x
theorem
DifferentiableOn.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableOn 𝕜 c s)
(f : F)
:
DifferentiableOn 𝕜 (fun (y : E) => c y • f) s
theorem
Differentiable.smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : Differentiable 𝕜 c)
(f : F)
:
Differentiable 𝕜 fun (y : E) => c y • f
theorem
fderivWithin_smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{s : Set E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(f : F)
:
theorem
fderiv_smul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{x : E}
{𝕜' : Type u_5}
[NontriviallyNormedField 𝕜']
[NormedAlgebra 𝕜 𝕜']
[NormedSpace 𝕜' F]
[IsScalarTower 𝕜 𝕜' F]
{c : E → 𝕜'}
(hc : DifferentiableAt 𝕜 c x)
(f : F)
:
Derivative of the product of two functions #
theorem
HasStrictFDerivAt.fun_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
{x : E}
(ha : HasStrictFDerivAt a a' x)
(hb : HasStrictFDerivAt b b' x)
:
HasStrictFDerivAt (fun (y : E) => a y * b y) (a x • b' + MulOpposite.op (b x) • a') x
theorem
HasStrictFDerivAt.mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
{x : E}
(ha : HasStrictFDerivAt a a' x)
(hb : HasStrictFDerivAt b b' x)
:
HasStrictFDerivAt (a * b) (a x • b' + MulOpposite.op (b x) • a') x
theorem
HasStrictFDerivAt.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasStrictFDerivAt c c' x)
(hd : HasStrictFDerivAt d d' x)
:
HasStrictFDerivAt (fun (y : E) => c y * d y) (c x • d' + d x • c') x
theorem
HasStrictFDerivAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasStrictFDerivAt c c' x)
(hd : HasStrictFDerivAt d d' x)
:
HasStrictFDerivAt (c * d) (c x • d' + d x • c') x
theorem
HasFDerivWithinAt.fun_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : HasFDerivWithinAt a a' s x)
(hb : HasFDerivWithinAt b b' s x)
:
HasFDerivWithinAt (fun (y : E) => a y * b y) (a x • b' + MulOpposite.op (b x) • a') s x
theorem
HasFDerivWithinAt.mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : HasFDerivWithinAt a a' s x)
(hb : HasFDerivWithinAt b b' s x)
:
HasFDerivWithinAt (a * b) (a x • b' + MulOpposite.op (b x) • a') s x
theorem
HasFDerivWithinAt.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasFDerivWithinAt c c' s x)
(hd : HasFDerivWithinAt d d' s x)
:
HasFDerivWithinAt (fun (y : E) => c y * d y) (c x • d' + d x • c') s x
theorem
HasFDerivWithinAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasFDerivWithinAt c c' s x)
(hd : HasFDerivWithinAt d d' s x)
:
HasFDerivWithinAt (c * d) (c x • d' + d x • c') s x
theorem
HasFDerivAt.fun_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : HasFDerivAt a a' x)
(hb : HasFDerivAt b b' x)
:
HasFDerivAt (fun (y : E) => a y * b y) (a x • b' + MulOpposite.op (b x) • a') x
theorem
HasFDerivAt.mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
{a' b' : E →L[𝕜] 𝔸}
(ha : HasFDerivAt a a' x)
(hb : HasFDerivAt b b' x)
:
HasFDerivAt (a * b) (a x • b' + MulOpposite.op (b x) • a') x
theorem
HasFDerivAt.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasFDerivAt c c' x)
(hd : HasFDerivAt d d' x)
:
HasFDerivAt (fun (y : E) => c y * d y) (c x • d' + d x • c') x
theorem
HasFDerivAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
{c' d' : E →L[𝕜] 𝔸'}
(hc : HasFDerivAt c c' x)
(hd : HasFDerivAt d d' x)
:
HasFDerivAt (c * d) (c x • d' + d x • c') x
theorem
DifferentiableWithinAt.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x)
:
DifferentiableWithinAt 𝕜 (fun (y : E) => a y * b y) s x
theorem
DifferentiableWithinAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x)
:
DifferentiableWithinAt 𝕜 (a * b) s x
@[simp]
theorem
DifferentiableAt.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(hb : DifferentiableAt 𝕜 b x)
:
DifferentiableAt 𝕜 (fun (y : E) => a y * b y) x
@[simp]
theorem
DifferentiableAt.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(hb : DifferentiableAt 𝕜 b x)
:
DifferentiableAt 𝕜 (a * b) x
theorem
DifferentiableOn.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableOn 𝕜 a s)
(hb : DifferentiableOn 𝕜 b s)
:
DifferentiableOn 𝕜 (fun (y : E) => a y * b y) s
theorem
DifferentiableOn.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableOn 𝕜 a s)
(hb : DifferentiableOn 𝕜 b s)
:
DifferentiableOn 𝕜 (a * b) s
@[simp]
theorem
Differentiable.fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : Differentiable 𝕜 a)
(hb : Differentiable 𝕜 b)
:
Differentiable 𝕜 fun (y : E) => a y * b y
@[simp]
theorem
Differentiable.mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : Differentiable 𝕜 a)
(hb : Differentiable 𝕜 b)
:
Differentiable 𝕜 (a * b)
theorem
fderivWithin_fun_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x)
:
fderivWithin 𝕜 (fun (y : E) => a y * b y) s x = a x • fderivWithin 𝕜 b s x + MulOpposite.op (b x) • fderivWithin 𝕜 a s x
theorem
fderivWithin_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(ha : DifferentiableWithinAt 𝕜 a s x)
(hb : DifferentiableWithinAt 𝕜 b s x)
:
fderivWithin 𝕜 (a * b) s x = a x • fderivWithin 𝕜 b s x + MulOpposite.op (b x) • fderivWithin 𝕜 a s x
theorem
fderivWithin_fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x)
:
fderivWithin 𝕜 (fun (y : E) => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x
theorem
fderivWithin_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(hd : DifferentiableWithinAt 𝕜 d s x)
:
theorem
fderiv_fun_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(hb : DifferentiableAt 𝕜 b x)
:
theorem
fderiv_mul'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a b : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(hb : DifferentiableAt 𝕜 b x)
:
theorem
fderiv_fun_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hc : DifferentiableAt 𝕜 c x)
(hd : DifferentiableAt 𝕜 d x)
:
theorem
fderiv_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c d : E → 𝔸'}
(hc : DifferentiableAt 𝕜 c x)
(hd : DifferentiableAt 𝕜 d x)
:
theorem
HasStrictFDerivAt.mul_const'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasStrictFDerivAt a a' x)
(b : 𝔸)
:
HasStrictFDerivAt (fun (y : E) => a y * b) (MulOpposite.op b • a') x
theorem
HasStrictFDerivAt.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c : E → 𝔸'}
{c' : E →L[𝕜] 𝔸'}
(hc : HasStrictFDerivAt c c' x)
(d : 𝔸')
:
HasStrictFDerivAt (fun (y : E) => c y * d) (d • c') x
theorem
HasFDerivWithinAt.mul_const'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasFDerivWithinAt a a' s x)
(b : 𝔸)
:
HasFDerivWithinAt (fun (y : E) => a y * b) (MulOpposite.op b • a') s x
theorem
HasFDerivWithinAt.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c : E → 𝔸'}
{c' : E →L[𝕜] 𝔸'}
(hc : HasFDerivWithinAt c c' s x)
(d : 𝔸')
:
HasFDerivWithinAt (fun (y : E) => c y * d) (d • c') s x
theorem
HasFDerivAt.mul_const'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasFDerivAt a a' x)
(b : 𝔸)
:
HasFDerivAt (fun (y : E) => a y * b) (MulOpposite.op b • a') x
theorem
HasFDerivAt.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c : E → 𝔸'}
{c' : E →L[𝕜] 𝔸'}
(hc : HasFDerivAt c c' x)
(d : 𝔸')
:
HasFDerivAt (fun (y : E) => c y * d) (d • c') x
theorem
DifferentiableWithinAt.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableWithinAt 𝕜 a s x)
(b : 𝔸)
:
DifferentiableWithinAt 𝕜 (fun (y : E) => a y * b) s x
theorem
DifferentiableAt.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(b : 𝔸)
:
DifferentiableAt 𝕜 (fun (y : E) => a y * b) x
theorem
DifferentiableOn.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableOn 𝕜 a s)
(b : 𝔸)
:
DifferentiableOn 𝕜 (fun (y : E) => a y * b) s
theorem
Differentiable.mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : Differentiable 𝕜 a)
(b : 𝔸)
:
Differentiable 𝕜 fun (y : E) => a y * b
theorem
fderivWithin_mul_const'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(ha : DifferentiableWithinAt 𝕜 a s x)
(b : 𝔸)
:
theorem
fderivWithin_mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c : E → 𝔸'}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hc : DifferentiableWithinAt 𝕜 c s x)
(d : 𝔸')
:
theorem
fderiv_mul_const'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(b : 𝔸)
:
theorem
fderiv_mul_const
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸' : Type u_6}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{c : E → 𝔸'}
(hc : DifferentiableAt 𝕜 c x)
(d : 𝔸')
:
theorem
HasStrictFDerivAt.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasStrictFDerivAt a a' x)
(b : 𝔸)
:
HasStrictFDerivAt (fun (y : E) => b * a y) (b • a') x
theorem
HasFDerivWithinAt.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasFDerivWithinAt a a' s x)
(b : 𝔸)
:
HasFDerivWithinAt (fun (y : E) => b * a y) (b • a') s x
theorem
HasFDerivAt.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
{a' : E →L[𝕜] 𝔸}
(ha : HasFDerivAt a a' x)
(b : 𝔸)
:
HasFDerivAt (fun (y : E) => b * a y) (b • a') x
theorem
DifferentiableWithinAt.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableWithinAt 𝕜 a s x)
(b : 𝔸)
:
DifferentiableWithinAt 𝕜 (fun (y : E) => b * a y) s x
theorem
DifferentiableAt.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(b : 𝔸)
:
DifferentiableAt 𝕜 (fun (y : E) => b * a y) x
theorem
DifferentiableOn.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableOn 𝕜 a s)
(b : 𝔸)
:
DifferentiableOn 𝕜 (fun (y : E) => b * a y) s
theorem
Differentiable.const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : Differentiable 𝕜 a)
(b : 𝔸)
:
Differentiable 𝕜 fun (y : E) => b * a y
theorem
fderivWithin_const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{s : Set E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(ha : DifferentiableWithinAt 𝕜 a s x)
(b : 𝔸)
:
theorem
fderiv_const_mul
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{x : E}
{𝔸 : Type u_5}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{a : E → 𝔸}
(ha : DifferentiableAt 𝕜 a x)
(b : 𝔸)
:
Derivative of a finite product of functions #
theorem
hasStrictFDerivAt_list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
[Fintype ι]
{l : List ι}
{x : ι → 𝔸}
:
theorem
hasStrictFDerivAt_list_prod_finRange'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{n : ℕ}
{x : Fin n → 𝔸}
:
HasStrictFDerivAt (fun (x : Fin n → 𝔸) => (List.map x (List.finRange n)).prod)
(∑ i : Fin n,
(List.map x (List.take (↑i) (List.finRange n))).prod • MulOpposite.op (List.map x (List.drop (↑i).succ (List.finRange n))).prod • ContinuousLinearMap.proj i)
x
theorem
hasStrictFDerivAt_list_prod_attach'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{l : List ι}
{x : { i : ι // i ∈ l } → 𝔸}
:
theorem
hasFDerivAt_list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
[Fintype ι]
{l : List ι}
{x : ι → 𝔸'}
:
theorem
hasFDerivAt_list_prod_finRange'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{n : ℕ}
{x : Fin n → 𝔸}
:
HasFDerivAt (fun (x : Fin n → 𝔸) => (List.map x (List.finRange n)).prod)
(∑ i : Fin n,
(List.map x (List.take (↑i) (List.finRange n))).prod • MulOpposite.op (List.map x (List.drop (↑i).succ (List.finRange n))).prod • ContinuousLinearMap.proj i)
x
theorem
hasFDerivAt_list_prod_attach'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{l : List ι}
{x : { i : ι // i ∈ l } → 𝔸}
:
theorem
hasStrictFDerivAt_list_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
[DecidableEq ι]
[Fintype ι]
{l : List ι}
{x : ι → 𝔸'}
:
HasStrictFDerivAt (fun (x : ι → 𝔸') => (List.map x l).prod)
(List.map (fun (i : ι) => (List.map x (l.erase i)).prod • ContinuousLinearMap.proj i) l).sum x
Auxiliary lemma for hasStrictFDerivAt_multiset_prod.
For NormedCommRing 𝔸', can rewrite as Multiset using Multiset.prod_coe.
theorem
hasStrictFDerivAt_multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
[DecidableEq ι]
[Fintype ι]
{u : Multiset ι}
{x : ι → 𝔸'}
:
HasStrictFDerivAt (fun (x : ι → 𝔸') => (Multiset.map x u).prod)
(Multiset.map (fun (i : ι) => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
theorem
hasFDerivAt_multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
[DecidableEq ι]
[Fintype ι]
{u : Multiset ι}
{x : ι → 𝔸'}
:
HasFDerivAt (fun (x : ι → 𝔸') => (Multiset.map x u).prod)
(Multiset.map (fun (i : ι) => (Multiset.map x (u.erase i)).prod • ContinuousLinearMap.proj i) u).sum x
theorem
hasStrictFDerivAt_finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
[DecidableEq ι]
[Fintype ι]
{x : ι → 𝔸'}
:
HasStrictFDerivAt (fun (x : ι → 𝔸') => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
theorem
hasFDerivAt_finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
[DecidableEq ι]
[Fintype ι]
{x : ι → 𝔸'}
:
HasFDerivAt (fun (x : ι → 𝔸') => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
theorem
HasStrictFDerivAt.list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : ι → E → 𝔸}
{f' : ι → E →L[𝕜] 𝔸}
{l : List ι}
{x : E}
(h : ∀ i ∈ l, HasStrictFDerivAt (fun (x : E) => f i x) (f' i) x)
:
theorem
HasFDerivAt.list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : ι → E → 𝔸}
{f' : ι → E →L[𝕜] 𝔸}
{l : List ι}
{x : E}
(h : ∀ i ∈ l, HasFDerivAt (fun (x : E) => f i x) (f' i) x)
:
Unlike HasFDerivAt.finset_prod, supports non-commutative multiply and duplicate elements.
theorem
HasFDerivWithinAt.list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : ι → E → 𝔸}
{f' : ι → E →L[𝕜] 𝔸}
{l : List ι}
{x : E}
(h : ∀ i ∈ l, HasFDerivWithinAt (fun (x : E) => f i x) (f' i) s x)
:
theorem
fderiv_list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : ι → E → 𝔸}
{l : List ι}
{x : E}
(h : ∀ i ∈ l, DifferentiableAt 𝕜 (fun (x : E) => f i x) x)
:
theorem
fderivWithin_list_prod'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸 : Type u_6}
[NormedRing 𝔸]
[NormedAlgebra 𝕜 𝔸]
{f : ι → E → 𝔸}
{l : List ι}
{x : E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(h : ∀ i ∈ l, DifferentiableWithinAt 𝕜 (fun (x : E) => f i x) s x)
:
theorem
HasStrictFDerivAt.multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{u : Multiset ι}
{x : E}
(h : ∀ i ∈ u, HasStrictFDerivAt (fun (x : E) => g i x) (g' i) x)
:
HasStrictFDerivAt (fun (x : E) => (Multiset.map (fun (x_1 : ι) => g x_1 x) u).prod)
(Multiset.map (fun (i : ι) => (Multiset.map (fun (x_1 : ι) => g x_1 x) (u.erase i)).prod • g' i) u).sum x
theorem
HasFDerivAt.multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{u : Multiset ι}
{x : E}
(h : ∀ i ∈ u, HasFDerivAt (fun (x : E) => g i x) (g' i) x)
:
HasFDerivAt (fun (x : E) => (Multiset.map (fun (x_1 : ι) => g x_1 x) u).prod)
(Multiset.map (fun (i : ι) => (Multiset.map (fun (x_1 : ι) => g x_1 x) (u.erase i)).prod • g' i) u).sum x
Unlike HasFDerivAt.finset_prod, supports duplicate elements.
theorem
HasFDerivWithinAt.multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{u : Multiset ι}
{x : E}
(h : ∀ i ∈ u, HasFDerivWithinAt (fun (x : E) => g i x) (g' i) s x)
:
HasFDerivWithinAt (fun (x : E) => (Multiset.map (fun (x_1 : ι) => g x_1 x) u).prod)
(Multiset.map (fun (i : ι) => (Multiset.map (fun (x_1 : ι) => g x_1 x) (u.erase i)).prod • g' i) u).sum s x
theorem
fderiv_multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{g : ι → E → 𝔸'}
[DecidableEq ι]
{u : Multiset ι}
{x : E}
(h : ∀ i ∈ u, DifferentiableAt 𝕜 (fun (x : E) => g i x) x)
:
fderiv 𝕜 (fun (x : E) => (Multiset.map (fun (x_1 : ι) => g x_1 x) u).prod) x = (Multiset.map (fun (i : ι) => (Multiset.map (fun (x_1 : ι) => g x_1 x) (u.erase i)).prod • fderiv 𝕜 (g i) x) u).sum
theorem
fderivWithin_multiset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{g : ι → E → 𝔸'}
[DecidableEq ι]
{u : Multiset ι}
{x : E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (fun (x : E) => g i x) s x)
:
fderivWithin 𝕜 (fun (x : E) => (Multiset.map (fun (x_1 : ι) => g x_1 x) u).prod) s x = (Multiset.map (fun (i : ι) => (Multiset.map (fun (x_1 : ι) => g x_1 x) (u.erase i)).prod • fderivWithin 𝕜 (g i) s x)
u).sum
theorem
HasStrictFDerivAt.finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{x : E}
(hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x)
:
HasStrictFDerivAt (fun (x : E) => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
theorem
HasFDerivAt.finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{x : E}
(hg : ∀ i ∈ u, HasFDerivAt (g i) (g' i) x)
:
HasFDerivAt (fun (x : E) => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x
theorem
HasFDerivWithinAt.finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{g : ι → E → 𝔸'}
{g' : ι → E →L[𝕜] 𝔸'}
[DecidableEq ι]
{x : E}
(hg : ∀ i ∈ u, HasFDerivWithinAt (g i) (g' i) s x)
:
HasFDerivWithinAt (fun (x : E) => ∏ i ∈ u, g i x) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) s x
theorem
fderiv_finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{g : ι → E → 𝔸'}
[DecidableEq ι]
{x : E}
(hg : ∀ i ∈ u, DifferentiableAt 𝕜 (g i) x)
:
theorem
fderivWithin_finset_prod
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{s : Set E}
{ι : Type u_5}
{𝔸' : Type u_7}
[NormedCommRing 𝔸']
[NormedAlgebra 𝕜 𝔸']
{u : Finset ι}
{g : ι → E → 𝔸'}
[DecidableEq ι]
{x : E}
(hxs : UniqueDiffWithinAt 𝕜 s x)
(hg : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (g i) s x)
:
fderivWithin 𝕜 (fun (x : E) => ∏ i ∈ u, g i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderivWithin 𝕜 (g i) s x
theorem
hasFDerivAt_ringInverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
(x : Rˣ)
:
HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
At an invertible element x of a normed algebra R, the Fréchet derivative of the inversion
operation is the linear map fun t ↦ - x⁻¹ * t * x⁻¹.
TODO (low prio): prove a version without assumption [HasSummableGeomSeries R] but within the set
of units.
@[deprecated hasFDerivAt_ringInverse (since := "2025-04-22")]
theorem
hasFDerivAt_ring_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
(x : Rˣ)
:
HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
Alias of hasFDerivAt_ringInverse.
At an invertible element x of a normed algebra R, the Fréchet derivative of the inversion
operation is the linear map fun t ↦ - x⁻¹ * t * x⁻¹.
TODO (low prio): prove a version without assumption [HasSummableGeomSeries R] but within the set
of units.
theorem
differentiableAt_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : IsUnit x)
:
theorem
differentiableWithinAt_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : IsUnit x)
(s : Set R)
:
theorem
differentiableOn_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
:
DifferentiableOn 𝕜 Ring.inverse {x : R | IsUnit x}
theorem
fderiv_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
(x : Rˣ)
:
theorem
hasStrictFDerivAt_ringInverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
(x : Rˣ)
:
HasStrictFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
@[deprecated hasStrictFDerivAt_ringInverse (since := "2025-04-22")]
theorem
hasStrictFDerivAt_ring_inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
(x : Rˣ)
:
HasStrictFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
Alias of hasStrictFDerivAt_ringInverse.
theorem
DifferentiableWithinAt.inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
{S : Set E}
(hf : DifferentiableWithinAt 𝕜 h S z)
(hz : IsUnit (h z))
:
DifferentiableWithinAt 𝕜 (fun (x : E) => Ring.inverse (h x)) S z
@[simp]
theorem
DifferentiableAt.inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
(hf : DifferentiableAt 𝕜 h z)
(hz : IsUnit (h z))
:
DifferentiableAt 𝕜 (fun (x : E) => Ring.inverse (h x)) z
theorem
DifferentiableOn.inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{S : Set E}
(hf : DifferentiableOn 𝕜 h S)
(hz : ∀ x ∈ S, IsUnit (h x))
:
DifferentiableOn 𝕜 (fun (x : E) => Ring.inverse (h x)) S
@[simp]
theorem
Differentiable.inverse
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedRing R]
[HasSummableGeomSeries R]
[NormedAlgebra 𝕜 R]
{h : E → R}
(hf : Differentiable 𝕜 h)
(hz : ∀ (x : E), IsUnit (h x))
:
Differentiable 𝕜 fun (x : E) => Ring.inverse (h x)
Derivative of the inverse in a division ring #
Note that some lemmas are primed as they are expressed without commutativity, whereas their
counterparts in commutative fields involve simpler expressions, and are given in
Mathlib/Analysis/Calculus/Deriv/Inv.lean.
theorem
hasStrictFDerivAt_inv'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : x ≠ 0)
:
HasStrictFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
At an invertible element x of a normed division algebra R, the inversion is strictly
differentiable, with derivative the linear map fun t ↦ - x⁻¹ * t * x⁻¹. For a nicer formula in
the commutative case, see hasStrictFDerivAt_inv.
theorem
hasFDerivAt_inv'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : x ≠ 0)
:
HasFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
At an invertible element x of a normed division algebra R, the Fréchet derivative of the
inversion operation is the linear map fun t ↦ - x⁻¹ * t * x⁻¹. For a nicer formula in the
commutative case, see hasFDerivAt_inv.
theorem
differentiableAt_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : x ≠ 0)
:
theorem
differentiableWithinAt_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : x ≠ 0)
(s : Set R)
:
DifferentiableWithinAt 𝕜 (fun (x : R) => x⁻¹) s x
theorem
differentiableOn_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
:
theorem
fderiv_inv'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{x : R}
(hx : x ≠ 0)
:
Non-commutative version of fderiv_inv
theorem
fderivWithin_inv'
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{s : Set R}
{x : R}
(hx : x ≠ 0)
(hxs : UniqueDiffWithinAt 𝕜 s x)
:
Non-commutative version of fderivWithin_inv
theorem
DifferentiableWithinAt.fun_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
{S : Set E}
(hf : DifferentiableWithinAt 𝕜 h S z)
(hz : h z ≠ 0)
:
DifferentiableWithinAt 𝕜 (fun (x : E) => (h x)⁻¹) S z
theorem
DifferentiableWithinAt.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
{S : Set E}
(hf : DifferentiableWithinAt 𝕜 h S z)
(hz : h z ≠ 0)
:
DifferentiableWithinAt 𝕜 h⁻¹ S z
@[simp]
theorem
DifferentiableAt.fun_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
(hf : DifferentiableAt 𝕜 h z)
(hz : h z ≠ 0)
:
DifferentiableAt 𝕜 (fun (x : E) => (h x)⁻¹) z
@[simp]
theorem
DifferentiableAt.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{z : E}
(hf : DifferentiableAt 𝕜 h z)
(hz : h z ≠ 0)
:
DifferentiableAt 𝕜 h⁻¹ z
theorem
DifferentiableOn.fun_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{S : Set E}
(hf : DifferentiableOn 𝕜 h S)
(hz : ∀ x ∈ S, h x ≠ 0)
:
DifferentiableOn 𝕜 (fun (x : E) => (h x)⁻¹) S
theorem
DifferentiableOn.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
{S : Set E}
(hf : DifferentiableOn 𝕜 h S)
(hz : ∀ x ∈ S, h x ≠ 0)
:
DifferentiableOn 𝕜 h⁻¹ S
@[simp]
theorem
Differentiable.fun_inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
(hf : Differentiable 𝕜 h)
(hz : ∀ (x : E), h x ≠ 0)
:
Differentiable 𝕜 fun (x : E) => (h x)⁻¹
@[simp]
theorem
Differentiable.inv
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{R : Type u_5}
[NormedDivisionRing R]
[NormedAlgebra 𝕜 R]
{h : E → R}
(hf : Differentiable 𝕜 h)
(hz : ∀ (x : E), h x ≠ 0)
:
Differentiable 𝕜 h⁻¹