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
multiplication of two scalar functions
inverse function (assuming that it exists; the inverse function theorem is in Mathlib/Analysis/Calculus/Inverse.lean)

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

source

theorem HasStrictFDerivAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :

HasStrictFDerivAt (fun y => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp (↑(ContinuousLinearMap.compL 𝕜 F G H) (c x)) d' + ContinuousLinearMap.comp (↑(ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 F G H)) (d x)) c') x

source

theorem HasFDerivWithinAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :

HasFDerivWithinAt (fun y => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp (↑(ContinuousLinearMap.compL 𝕜 F G H) (c x)) d' + ContinuousLinearMap.comp (↑(ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 F G H)) (d x)) c') s x

source

theorem HasFDerivAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {d : E → F →L[𝕜] G} {d' : E →L[𝕜] F →L[𝕜] G} (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :

HasFDerivAt (fun y => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp (↑(ContinuousLinearMap.compL 𝕜 F G H) (c x)) d' + ContinuousLinearMap.comp (↑(ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 F G H)) (d x)) c') x

source

theorem DifferentiableWithinAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :

DifferentiableWithinAt 𝕜 (fun y => ContinuousLinearMap.comp (c y) (d y)) s x

source

theorem DifferentiableAt.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :

DifferentiableAt 𝕜 (fun y => ContinuousLinearMap.comp (c y) (d y)) x

source

theorem DifferentiableOn.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : DifferentiableOn 𝕜 c s) (hd : DifferentiableOn 𝕜 d s) :

DifferentiableOn 𝕜 (fun y => ContinuousLinearMap.comp (c y) (d y)) s

source

theorem Differentiable.clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) :

Differentiable 𝕜 fun y => ContinuousLinearMap.comp (c y) (d y)

source

theorem fderivWithin_clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :

fderivWithin 𝕜 (fun y => ContinuousLinearMap.comp (c y) (d y)) s x = ContinuousLinearMap.comp (↑(ContinuousLinearMap.compL 𝕜 F G H) (c x)) (fderivWithin 𝕜 d s x) + ContinuousLinearMap.comp (↑(ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 F G H)) (d x)) (fderivWithin 𝕜 c s x)

source

theorem fderiv_clm_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :

fderiv 𝕜 (fun y => ContinuousLinearMap.comp (c y) (d y)) x = ContinuousLinearMap.comp (↑(ContinuousLinearMap.compL 𝕜 F G H) (c x)) (fderiv 𝕜 d x) + ContinuousLinearMap.comp (↑(ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 F G H)) (d x)) (fderiv 𝕜 c x)

source

theorem HasStrictFDerivAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {u : E → G} {u' : E →L[𝕜] G} (hc : HasStrictFDerivAt c c' x) (hu : HasStrictFDerivAt u u' x) :

HasStrictFDerivAt (fun y => ↑(c y) (u y)) (ContinuousLinearMap.comp (c x) u' + ↑(ContinuousLinearMap.flip c') (u x)) x

source

theorem HasFDerivWithinAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {u : E → G} {u' : E →L[𝕜] G} (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) :

HasFDerivWithinAt (fun y => ↑(c y) (u y)) (ContinuousLinearMap.comp (c x) u' + ↑(ContinuousLinearMap.flip c') (u x)) s x

source

theorem HasFDerivAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H} {u : E → G} {u' : E →L[𝕜] G} (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :

HasFDerivAt (fun y => ↑(c y) (u y)) (ContinuousLinearMap.comp (c x) u' + ↑(ContinuousLinearMap.flip c') (u x)) x

source

theorem DifferentiableWithinAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :

DifferentiableWithinAt 𝕜 (fun y => ↑(c y) (u y)) s x

source

theorem DifferentiableAt.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :

DifferentiableAt 𝕜 (fun y => ↑(c y) (u y)) x

source

theorem DifferentiableOn.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableOn 𝕜 c s) (hu : DifferentiableOn 𝕜 u s) :

DifferentiableOn 𝕜 (fun y => ↑(c y) (u y)) s

source

theorem Differentiable.clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : Differentiable 𝕜 c) (hu : Differentiable 𝕜 u) :

Differentiable 𝕜 fun y => ↑(c y) (u y)

source

theorem fderivWithin_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hu : DifferentiableWithinAt 𝕜 u s x) :

fderivWithin 𝕜 (fun y => ↑(c y) (u y)) s x = ContinuousLinearMap.comp (c x) (fderivWithin 𝕜 u s x) + ↑(ContinuousLinearMap.flip (fderivWithin 𝕜 c s x)) (u x)

source

theorem fderiv_clm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :

fderiv 𝕜 (fun y => ↑(c y) (u y)) x = ContinuousLinearMap.comp (c x) (fderiv 𝕜 u x) + ↑(ContinuousLinearMap.flip (fderiv 𝕜 c x)) (u x)

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.

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :

HasStrictFDerivAt (fun y => c y • f y) (c x • f' + ContinuousLinearMap.smulRight c' (f x)) x

source

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_6} [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 => c y • f y) (c x • f' + ContinuousLinearMap.smulRight c' (f x)) s x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :

HasFDerivAt (fun y => c y • f y) (c x • f' + ContinuousLinearMap.smulRight c' (f x)) x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (hf : DifferentiableWithinAt 𝕜 f s x) :

DifferentiableWithinAt 𝕜 (fun y => c y • f y) s x

source

@[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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :

DifferentiableAt 𝕜 (fun y => c y • f y) x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableOn 𝕜 c s) (hf : DifferentiableOn 𝕜 f s) :

DifferentiableOn 𝕜 (fun y => c y • f y) s

source

@[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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : Differentiable 𝕜 c) (hf : Differentiable 𝕜 f) :

Differentiable 𝕜 fun y => c y • f y

source

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_6} [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 => c y • f y) s x = c x • fderivWithin 𝕜 f s x + ContinuousLinearMap.smulRight (fderivWithin 𝕜 c s x) (f x)

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (hf : DifferentiableAt 𝕜 f x) :

fderiv 𝕜 (fun y => c y • f y) x = c x • fderiv 𝕜 f x + ContinuousLinearMap.smulRight (fderiv 𝕜 c x) (f x)

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : HasStrictFDerivAt c c' x) (f : F) :

HasStrictFDerivAt (fun y => c y • f) (ContinuousLinearMap.smulRight c' f) x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : HasFDerivWithinAt c c' s x) (f : F) :

HasFDerivWithinAt (fun y => c y • f) (ContinuousLinearMap.smulRight c' f) s x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'} (hc : HasFDerivAt c c' x) (f : F) :

HasFDerivAt (fun y => c y • f) (ContinuousLinearMap.smulRight c' f) x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :

DifferentiableWithinAt 𝕜 (fun y => c y • f) s x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (f : F) :

DifferentiableAt 𝕜 (fun y => c y • f) x

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableOn 𝕜 c s) (f : F) :

DifferentiableOn 𝕜 (fun y => c y • f) s

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : Differentiable 𝕜 c) (f : F) :

Differentiable 𝕜 fun y => c y • f

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (f : F) :

fderivWithin 𝕜 (fun y => c y • f) s x = ContinuousLinearMap.smulRight (fderivWithin 𝕜 c s x) f

source

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_6} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (f : F) :

fderiv 𝕜 (fun y => c y • f) x = ContinuousLinearMap.smulRight (fderiv 𝕜 c x) f

Derivative of the product of two functions #

source

theorem HasStrictFDerivAt.mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} {a' : E →L[𝕜] 𝔸} {b' : E →L[𝕜] 𝔸} {x : E} (ha : HasStrictFDerivAt a a' x) (hb : HasStrictFDerivAt b b' x) :

HasStrictFDerivAt (fun y => a y * b y) (a x • b' + ContinuousLinearMap.smulRight a' (b x)) x

source

theorem HasStrictFDerivAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {d : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} {d' : E →L[𝕜] 𝔸'} (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :

HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

source

theorem HasFDerivWithinAt.mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} {a' : E →L[𝕜] 𝔸} {b' : E →L[𝕜] 𝔸} (ha : HasFDerivWithinAt a a' s x) (hb : HasFDerivWithinAt b b' s x) :

HasFDerivWithinAt (fun y => a y * b y) (a x • b' + ContinuousLinearMap.smulRight a' (b x)) s x

source

theorem HasFDerivWithinAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {d : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} {d' : E →L[𝕜] 𝔸'} (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :

HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x

source

theorem HasFDerivAt.mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} {a' : E →L[𝕜] 𝔸} {b' : E →L[𝕜] 𝔸} (ha : HasFDerivAt a a' x) (hb : HasFDerivAt b b' x) :

HasFDerivAt (fun y => a y * b y) (a x • b' + ContinuousLinearMap.smulRight a' (b x)) x

source

theorem HasFDerivAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {d : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} {d' : E →L[𝕜] 𝔸'} (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :

HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x

source

theorem DifferentiableWithinAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (ha : DifferentiableWithinAt 𝕜 a s x) (hb : DifferentiableWithinAt 𝕜 b s x) :

DifferentiableWithinAt 𝕜 (fun y => a y * b y) s x

source

@[simp]

theorem DifferentiableAt.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :

DifferentiableAt 𝕜 (fun y => a y * b y) x

source

theorem DifferentiableOn.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) :

DifferentiableOn 𝕜 (fun y => a y * b y) s

source

@[simp]

theorem Differentiable.mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (ha : Differentiable 𝕜 a) (hb : Differentiable 𝕜 b) :

Differentiable 𝕜 fun y => a y * b y

source

theorem DifferentiableWithinAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableWithinAt 𝕜 a s x) (n : ℕ) :

DifferentiableWithinAt 𝕜 (fun x => a x ^ n) s x

source

@[simp]

theorem DifferentiableAt.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (n : ℕ) :

DifferentiableAt 𝕜 (fun x => a x ^ n) x

source

theorem DifferentiableOn.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (n : ℕ) :

DifferentiableOn 𝕜 (fun x => a x ^ n) s

source

@[simp]

theorem Differentiable.pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : Differentiable 𝕜 a) (n : ℕ) :

Differentiable 𝕜 fun x => a x ^ n

source

theorem fderivWithin_mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (hb : DifferentiableWithinAt 𝕜 b s x) :

fderivWithin 𝕜 (fun y => a y * b y) s x = a x • fderivWithin 𝕜 b s x + ContinuousLinearMap.smulRight (fderivWithin 𝕜 a s x) (b x)

source

theorem fderivWithin_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {d : E → 𝔸'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (hd : DifferentiableWithinAt 𝕜 d s x) :

fderivWithin 𝕜 (fun y => c y * d y) s x = c x • fderivWithin 𝕜 d s x + d x • fderivWithin 𝕜 c s x

source

theorem fderiv_mul' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {b : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (hb : DifferentiableAt 𝕜 b x) :

fderiv 𝕜 (fun y => a y * b y) x = a x • fderiv 𝕜 b x + ContinuousLinearMap.smulRight (fderiv 𝕜 a x) (b x)

source

theorem fderiv_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {d : E → 𝔸'} (hc : DifferentiableAt 𝕜 c x) (hd : DifferentiableAt 𝕜 d x) :

fderiv 𝕜 (fun y => c y * d y) x = c x • fderiv 𝕜 d x + d x • fderiv 𝕜 c x

source

theorem HasStrictFDerivAt.mul_const' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :

HasStrictFDerivAt (fun y => a y * b) (ContinuousLinearMap.smulRight a' b) x

source

theorem HasStrictFDerivAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : HasStrictFDerivAt c c' x) (d : 𝔸') :

HasStrictFDerivAt (fun y => c y * d) (d • c') x

source

theorem HasFDerivWithinAt.mul_const' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) :

HasFDerivWithinAt (fun y => a y * b) (ContinuousLinearMap.smulRight a' b) s x

source

theorem HasFDerivWithinAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : HasFDerivWithinAt c c' s x) (d : 𝔸') :

HasFDerivWithinAt (fun y => c y * d) (d • c') s x

source

theorem HasFDerivAt.mul_const' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasFDerivAt a a' x) (b : 𝔸) :

HasFDerivAt (fun y => a y * b) (ContinuousLinearMap.smulRight a' b) x

source

theorem HasFDerivAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} {c' : E →L[𝕜] 𝔸'} (hc : HasFDerivAt c c' x) (d : 𝔸') :

HasFDerivAt (fun y => c y * d) (d • c') x

source

theorem DifferentiableWithinAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :

DifferentiableWithinAt 𝕜 (fun y => a y * b) s x

source

theorem DifferentiableAt.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

DifferentiableAt 𝕜 (fun y => a y * b) x

source

theorem DifferentiableOn.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (b : 𝔸) :

DifferentiableOn 𝕜 (fun y => a y * b) s

source

theorem Differentiable.mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : Differentiable 𝕜 a) (b : 𝔸) :

Differentiable 𝕜 fun y => a y * b

source

theorem fderivWithin_mul_const' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :

fderivWithin 𝕜 (fun y => a y * b) s x = ContinuousLinearMap.smulRight (fderivWithin 𝕜 a s x) b

source

theorem fderivWithin_mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸') :

fderivWithin 𝕜 (fun y => c y * d) s x = d • fderivWithin 𝕜 c s x

source

theorem fderiv_mul_const' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

fderiv 𝕜 (fun y => a y * b) x = ContinuousLinearMap.smulRight (fderiv 𝕜 a x) b

source

theorem fderiv_mul_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} (hc : DifferentiableAt 𝕜 c x) (d : 𝔸') :

fderiv 𝕜 (fun y => c y * d) x = d • fderiv 𝕜 c x

source

theorem HasStrictFDerivAt.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :

HasStrictFDerivAt (fun y => b * a y) (b • a') x

source

theorem HasFDerivWithinAt.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) :

HasFDerivWithinAt (fun y => b * a y) (b • a') s x

source

theorem HasFDerivAt.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasFDerivAt a a' x) (b : 𝔸) :

HasFDerivAt (fun y => b * a y) (b • a') x

source

theorem DifferentiableWithinAt.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :

DifferentiableWithinAt 𝕜 (fun y => b * a y) s x

source

theorem DifferentiableAt.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

DifferentiableAt 𝕜 (fun y => b * a y) x

source

theorem DifferentiableOn.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (b : 𝔸) :

DifferentiableOn 𝕜 (fun y => b * a y) s

source

theorem Differentiable.const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : Differentiable 𝕜 a) (b : 𝔸) :

Differentiable 𝕜 fun y => b * a y

source

theorem fderivWithin_const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (hxs : UniqueDiffWithinAt 𝕜 s x) (ha : DifferentiableWithinAt 𝕜 a s x) (b : 𝔸) :

fderivWithin 𝕜 (fun y => b * a y) s x = b • fderivWithin 𝕜 a s x

source

theorem fderiv_const_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

fderiv 𝕜 (fun y => b * a y) x = b • fderiv 𝕜 a x

source

theorem hasFDerivAt_ring_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace 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: prove that Ring.inverse is analytic and use it to prove a HasStrictFDerivAt lemma. TODO (low prio): prove a version without assumption [CompleteSpace R] but within the set of units.

source

theorem differentiableAt_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {x : R} (hx : IsUnit x) :

DifferentiableAt 𝕜 Ring.inverse x

source

theorem differentiableWithinAt_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {x : R} (hx : IsUnit x) (s : Set R) :

DifferentiableWithinAt 𝕜 Ring.inverse s x

source

theorem differentiableOn_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] :

DifferentiableOn 𝕜 Ring.inverse {x | IsUnit x}

source

theorem fderiv_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] (x : Rˣ) :

fderiv 𝕜 Ring.inverse ↑x = -↑(↑(ContinuousLinearMap.mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹

source

theorem DifferentiableWithinAt.inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {z : E} {S : Set E} (hf : DifferentiableWithinAt 𝕜 h S z) (hz : IsUnit (h z)) :

DifferentiableWithinAt 𝕜 (fun x => Ring.inverse (h x)) S z

source

@[simp]

theorem DifferentiableAt.inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {z : E} (hf : DifferentiableAt 𝕜 h z) (hz : IsUnit (h z)) :

DifferentiableAt 𝕜 (fun x => Ring.inverse (h x)) z

source

theorem DifferentiableOn.inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {S : Set E} (hf : DifferentiableOn 𝕜 h S) (hz : ∀ (x : E), x ∈ S → IsUnit (h x)) :

DifferentiableOn 𝕜 (fun x => Ring.inverse (h x)) S

source

@[simp]

theorem Differentiable.inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} (hf : Differentiable 𝕜 h) (hz : ∀ (x : E), IsUnit (h x)) :

Differentiable 𝕜 fun x => Ring.inverse (h x)

Derivative of the inverse in a division ring #

Note these lemmas are primed as they need CompleteSpace R, whereas the other lemmas in Mathlib/Analysis/Calculus/Deriv/Inv.lean do not, but instead need NontriviallyNormedField R.

source

theorem hasFDerivAt_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace 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 λ t, - x⁻¹ * t * x⁻¹.

source

theorem differentiableAt_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {x : R} (hx : x ≠ 0) :

DifferentiableAt 𝕜 Inv.inv x

source

theorem differentiableWithinAt_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {x : R} (hx : x ≠ 0) (s : Set R) :

DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x

source

theorem differentiableOn_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] :

DifferentiableOn 𝕜 (fun x => x⁻¹) {x | x ≠ 0}

source

theorem fderiv_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {x : R} (hx : x ≠ 0) :

fderiv 𝕜 Inv.inv x = -↑(↑(ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Non-commutative version of fderiv_inv

source

theorem fderivWithin_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (fun x => x⁻¹) s x = -↑(↑(ContinuousLinearMap.mulLeftRight 𝕜 R) x⁻¹) x⁻¹

Non-commutative version of fderivWithin_inv

source

theorem DifferentiableWithinAt.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {z : E} {S : Set E} (hf : DifferentiableWithinAt 𝕜 h S z) (hz : h z ≠ 0) :

DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z

source

@[simp]

theorem DifferentiableAt.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {z : E} (hf : DifferentiableAt 𝕜 h z) (hz : h z ≠ 0) :

DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z

source

theorem DifferentiableOn.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} {S : Set E} (hf : DifferentiableOn 𝕜 h S) (hz : ∀ (x : E), x ∈ S → h x ≠ 0) :

DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S

source

@[simp]

theorem Differentiable.inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] [CompleteSpace R] {h : E → R} (hf : Differentiable 𝕜 h) (hz : ∀ (x : E), h x ≠ 0) :

Differentiable 𝕜 fun x => (h x)⁻¹