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.inv or Ring.inverse) of a function

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_5} [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 : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp 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_5} [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 : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp 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_5} [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 : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp d' + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp 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_5} [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 : E) => (c y).comp (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_5} [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 : E) => (c y).comp (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_5} [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 : E) => (c y).comp (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_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {d : E → F →L[𝕜] G} (hc : Differentiable 𝕜 c) (hd : Differentiable 𝕜 d) :

Differentiable 𝕜 fun (y : E) => (c y).comp (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_5} [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 : E) => (c y).comp (d y)) s x = ((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp (fderivWithin 𝕜 d s x) + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp (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_5} [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 : E) => (c y).comp (d y)) x = ((ContinuousLinearMap.compL 𝕜 F G H) (c x)).comp (fderiv 𝕜 d x) + ((ContinuousLinearMap.compL 𝕜 F G H).flip (d x)).comp (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_5} [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 : E) => (c y) (u y)) ((c x).comp u' + c'.flip (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_5} [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 : E) => (c y) (u y)) ((c x).comp u' + c'.flip (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_5} [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 : E) => (c y) (u y)) ((c x).comp u' + c'.flip (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_5} [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 : E) => (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_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :

DifferentiableAt 𝕜 (fun (y : E) => (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_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableOn 𝕜 c s) (hu : DifferentiableOn 𝕜 u s) :

DifferentiableOn 𝕜 (fun (y : E) => (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_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : Differentiable 𝕜 c) (hu : Differentiable 𝕜 u) :

Differentiable 𝕜 fun (y : E) => (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_5} [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 : E) => (c y) (u y)) s x = (c x).comp (fderivWithin 𝕜 u s x) + (fderivWithin 𝕜 c s x).flip (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_5} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G} (hc : DifferentiableAt 𝕜 c x) (hu : DifferentiableAt 𝕜 u x) :

fderiv 𝕜 (fun (y : E) => (c y) (u y)) x = (c x).comp (fderiv 𝕜 u x) + (fderiv 𝕜 c x).flip (u x)

Derivative of the application of continuous multilinear maps to a constant #

source

theorem HasStrictFDerivAt.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} (hc : HasStrictFDerivAt c c' x) (u : (i : ι) → M i) :

HasStrictFDerivAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) x

source

theorem HasFDerivWithinAt.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} (hc : HasFDerivWithinAt c c' s x) (u : (i : ι) → M i) :

HasFDerivWithinAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) s x

source

theorem HasFDerivAt.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} {c' : E →L[𝕜] ContinuousMultilinearMap 𝕜 M H} (hc : HasFDerivAt c c' x) (u : (i : ι) → M i) :

HasFDerivAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) x

source

theorem DifferentiableWithinAt.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : DifferentiableWithinAt 𝕜 c s x) (u : (i : ι) → M i) :

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

source

theorem DifferentiableAt.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : DifferentiableAt 𝕜 c x) (u : (i : ι) → M i) :

DifferentiableAt 𝕜 (fun (y : E) => (c y) u) x

source

theorem DifferentiableOn.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : DifferentiableOn 𝕜 c s) (u : (i : ι) → M i) :

DifferentiableOn 𝕜 (fun (y : E) => (c y) u) s

source

theorem Differentiable.continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : Differentiable 𝕜 c) (u : (i : ι) → M i) :

Differentiable 𝕜 fun (y : E) => (c y) u

source

theorem fderivWithin_continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (u : (i : ι) → M i) :

fderivWithin 𝕜 (fun (y : E) => (c y) u) s x = (fderivWithin 𝕜 c s x).flipMultilinear u

source

theorem fderiv_continuousMultilinear_apply_const {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : DifferentiableAt 𝕜 c x) (u : (i : ι) → M i) :

fderiv 𝕜 (fun (y : E) => (c y) u) x = (fderiv 𝕜 c x).flipMultilinear u

source

theorem fderivWithin_continuousMultilinear_apply_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (u : (i : ι) → M i) (m : E) :

(fderivWithin 𝕜 (fun (y : E) => (c y) u) s x) m = ((fderivWithin 𝕜 c s x) m) u

Application of a ContinuousMultilinearMap to a constant commutes with fderivWithin.

source

theorem fderiv_continuousMultilinear_apply_const_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {ι : Type u_5} [Fintype ι] {M : ι → Type u_6} [(i : ι) → NormedAddCommGroup (M i)] [(i : ι) → NormedSpace 𝕜 (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace 𝕜 H] {c : E → ContinuousMultilinearMap 𝕜 M H} (hc : DifferentiableAt 𝕜 c x) (u : (i : ι) → M i) (m : E) :

(fderiv 𝕜 (fun (y : E) => (c y) u) x) m = ((fderiv 𝕜 c x) m) u

Application of a ContinuousMultilinearMap to a constant commutes with fderiv.

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_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

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_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

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_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

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_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

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_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

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_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

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

Differentiable 𝕜 fun (y : E) => 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_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)

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

fderiv 𝕜 (fun (y : E) => c y • f y) x = c x • fderiv 𝕜 f x + (fderiv 𝕜 c x).smulRight (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_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

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_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

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_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

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_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

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

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

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

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

fderivWithin 𝕜 (fun (y : E) => c y • f) s x = (fderivWithin 𝕜 c s x).smulRight 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_5} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} (hc : DifferentiableAt 𝕜 c x) (f : F) :

fderiv 𝕜 (fun (y : E) => c y • f) x = (fderiv 𝕜 c x).smulRight 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_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' + a'.smulRight (b x)) x

source

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 (fun (y : E) => 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_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' + a'.smulRight (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_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

source

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 (fun (y : E) => a y * b y) (a x • b' + a'.smulRight (b x)) x

source

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 (fun (y : E) => 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_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

source

@[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 𝕜 (fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a b : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (hb : DifferentiableOn 𝕜 b s) :

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

source

@[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 𝕜 fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableWithinAt 𝕜 a s x) (n : ℕ) :

DifferentiableWithinAt 𝕜 (fun (x : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (n : ℕ) :

DifferentiableAt 𝕜 (fun (x : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableOn 𝕜 a s) (n : ℕ) :

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

source

@[simp]

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

Differentiable 𝕜 fun (x : E) => 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_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 + (fderivWithin 𝕜 a s x).smulRight (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_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

source

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) :

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

source

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) :

fderiv 𝕜 (fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :

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

source

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

source

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) (a'.smulRight 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_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

source

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) (a'.smulRight b) x

source

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

source

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

source

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

source

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

source

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

source

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 : 𝔸) :

fderivWithin 𝕜 (fun (y : E) => a y * b) s x = (fderivWithin 𝕜 a s x).smulRight 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} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] {c : E → 𝔸'} (hxs : UniqueDiffWithinAt 𝕜 s x) (hc : DifferentiableWithinAt 𝕜 c s x) (d : 𝔸') :

fderivWithin 𝕜 (fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

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

source

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 : 𝔸') :

fderiv 𝕜 (fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} {a' : E →L[𝕜] 𝔸} (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :

HasStrictFDerivAt (fun (y : E) => 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_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

source

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

source

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

source

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

source

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

source

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

source

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 : 𝔸) :

fderivWithin 𝕜 (fun (y : E) => 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_5} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] {a : E → 𝔸} (ha : DifferentiableAt 𝕜 a x) (b : 𝔸) :

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

Derivative of a finite product of functions #

source

theorem hasStrictFDerivAt_list_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [Fintype ι] {l : List ι} {x : ι → 𝔸} :

HasStrictFDerivAt (fun (x : ι → 𝔸) => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x

source

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 • (ContinuousLinearMap.proj i).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod) x

source

theorem hasStrictFDerivAt_list_prod_attach' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [DecidableEq ι] {l : List ι} {x : { i : ι // i ∈ l } → 𝔸} :

HasStrictFDerivAt (fun (x : { x : ι // x ∈ l } → 𝔸) => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x

source

theorem hasFDerivAt_list_prod' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra 𝕜 𝔸'] [Fintype ι] {l : List ι} {x : ι → 𝔸'} :

HasFDerivAt (fun (x : ι → 𝔸') => (List.map x l).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l)).prod • (ContinuousLinearMap.proj l[i]).smulRight (List.map x (List.drop (↑i).succ l)).prod) x

source

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 • (ContinuousLinearMap.proj i).smulRight (List.map x (List.drop (↑i).succ (List.finRange n))).prod) x

source

theorem hasFDerivAt_list_prod_attach' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra 𝕜 𝔸] [DecidableEq ι] {l : List ι} {x : { i : ι // i ∈ l } → 𝔸} :

HasFDerivAt (fun (x : { x : ι // x ∈ l } → 𝔸) => (List.map x l.attach).prod) (∑ i : Fin l.length, (List.map x (List.take (↑i) l.attach)).prod • (ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod) x

source

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.

source

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

source

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

source

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

source

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

source

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) :

HasStrictFDerivAt (fun (x : E) => (List.map (fun (x_1 : ι) => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun (x_1 : ι) => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun (x_1 : ι) => f x_1 x) (List.drop (↑i).succ l)).prod) x

source

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) :

HasFDerivAt (fun (x : E) => (List.map (fun (x_1 : ι) => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun (x_1 : ι) => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun (x_1 : ι) => f x_1 x) (List.drop (↑i).succ l)).prod) x

Unlike HasFDerivAt.finset_prod, supports non-commutative multiply and duplicate elements.

source

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) :

HasFDerivWithinAt (fun (x : E) => (List.map (fun (x_1 : ι) => f x_1 x) l).prod) (∑ i : Fin l.length, (List.map (fun (x_1 : ι) => f x_1 x) (List.take (↑i) l)).prod • (f' l[i]).smulRight (List.map (fun (x_1 : ι) => f x_1 x) (List.drop (↑i).succ l)).prod) s x

source

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) :

fderiv 𝕜 (fun (x : E) => (List.map (fun (x_1 : ι) => f x_1 x) l).prod) x = ∑ i : Fin l.length, (List.map (fun (x_1 : ι) => f x_1 x) (List.take (↑i) l)).prod • (fderiv 𝕜 (fun (x : E) => f l[i] x) x).smulRight (List.map (fun (x_1 : ι) => f x_1 x) (List.drop (↑i).succ l)).prod

source

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) :

fderivWithin 𝕜 (fun (x : E) => (List.map (fun (x_1 : ι) => f x_1 x) l).prod) s x = ∑ i : Fin l.length, (List.map (fun (x_1 : ι) => f x_1 x) (List.take (↑i) l)).prod • (fderivWithin 𝕜 (fun (x : E) => f l[i] x) s x).smulRight (List.map (fun (x_1 : ι) => f x_1 x) (List.drop (↑i).succ l)).prod

source

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

source

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.

source

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

source

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

source

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

source

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

source

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

source

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

source

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) :

fderiv 𝕜 (fun (x : E) => ∏ i ∈ u, g i x) x = ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • fderiv 𝕜 (g i) x

source

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

source

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

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.

source

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

DifferentiableAt 𝕜 Ring.inverse x

source

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) :

DifferentiableWithinAt 𝕜 Ring.inverse s x

source

theorem differentiableOn_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_5} [NormedRing R] [HasSummableGeomSeries R] [NormedAlgebra 𝕜 R] :

DifferentiableOn 𝕜 Ring.inverse {x : R | IsUnit x}

source

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

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

source

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

source

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

source

@[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

source

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

source

@[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.

source

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.

source

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.

source

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

DifferentiableAt 𝕜 Inv.inv x

source

@[deprecated differentiableAt_inv]

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

DifferentiableAt 𝕜 Inv.inv x

Alias of differentiableAt_inv.

source

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

source

@[deprecated differentiableWithinAt_inv]

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

Alias of differentiableWithinAt_inv.

source

theorem differentiableOn_inv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_5} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] :

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

source

@[deprecated differentiableOn_inv]

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

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

Alias of differentiableOn_inv.

source

theorem fderiv_inv' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_5} [NormedDivisionRing R] [NormedAlgebra 𝕜 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_5} [NormedDivisionRing R] [NormedAlgebra 𝕜 R] {s : Set R} {x : R} (hx : x ≠ 0) (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (fun (x : R) => 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_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

source

@[deprecated DifferentiableWithinAt.inv]

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 𝕜 (fun (x : E) => (h x)⁻¹) S z

Alias of DifferentiableWithinAt.inv.

source

@[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 𝕜 (fun (x : E) => (h x)⁻¹) z

source

@[deprecated DifferentiableAt.inv]

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 𝕜 (fun (x : E) => (h x)⁻¹) z

Alias of DifferentiableAt.inv.

source

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 𝕜 (fun (x : E) => (h x)⁻¹) S

source

@[deprecated DifferentiableOn.inv]

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 𝕜 (fun (x : E) => (h x)⁻¹) S

Alias of DifferentiableOn.inv.

source

@[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 𝕜 fun (x : E) => (h x)⁻¹

source

@[deprecated Differentiable.inv]

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 𝕜 fun (x : E) => (h x)⁻¹

Alias of Differentiable.inv.

HepLean Documentation

Mathlib.Analysis.Calculus.FDeriv.Mul

Multiplicative operations on derivatives #

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

Derivative of the application of continuous multilinear maps to a constant #

Derivative of the product of a scalar-valued function and a vector-valued function #

Derivative of the product of two functions #

Derivative of a finite product of functions #

Derivative of the inverse in a division ring #