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

theorem HasStrictFDerivAt.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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 : ) (hd : ) :
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
theorem HasFDerivWithinAt.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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
theorem HasFDerivAt.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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
theorem DifferentiableWithinAt.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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
theorem DifferentiableAt.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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
theorem DifferentiableOn.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {s : Set E} {H : Type u_6} [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
theorem Differentiable.clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {H : Type u_6} [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)
theorem fderivWithin_clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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)
theorem fderiv_clm_comp {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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)
theorem HasStrictFDerivAt.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [NormedSpace π H] {c : E β G βL[π] H} {c' : E βL[π] G βL[π] H} {u : E β G} {u' : E βL[π] G} (hc : ) (hu : ) :
HasStrictFDerivAt (fun (y : E) => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x
theorem HasFDerivWithinAt.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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
theorem HasFDerivAt.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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
theorem DifferentiableWithinAt.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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
theorem DifferentiableAt.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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
theorem DifferentiableOn.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {s : Set E} {H : Type u_6} [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
theorem Differentiable.clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {H : Type u_6} [NormedSpace π H] {c : E β G βL[π] H} {u : E β G} (hc : Differentiable π c) (hu : Differentiable π u) :
Differentiable π fun (y : E) => (c y) (u y)
theorem fderivWithin_clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {s : Set E} {H : Type u_6} [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)
theorem fderiv_clm_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {G : Type u_4} [NormedSpace π G] {x : E} {H : Type u_6} [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 #

theorem HasStrictFDerivAt.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [NormedSpace π H] {c : E β ContinuousMultilinearMap π M H} {c' : E βL[π] ContinuousMultilinearMap π M H} (hc : ) (u : (i : ΞΉ) β M i) :
HasStrictFDerivAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) x
theorem HasFDerivWithinAt.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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
theorem HasFDerivAt.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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
theorem DifferentiableWithinAt.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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
theorem DifferentiableAt.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [NormedSpace π H] {c : E β ContinuousMultilinearMap π M H} (hc : DifferentiableAt π c x) (u : (i : ΞΉ) β M i) :
DifferentiableAt π (fun (y : E) => (c y) u) x
theorem DifferentiableOn.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [NormedSpace π H] {c : E β ContinuousMultilinearMap π M H} (hc : DifferentiableOn π c s) (u : (i : ΞΉ) β M i) :
DifferentiableOn π (fun (y : E) => (c y) u) s
theorem Differentiable.continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [NormedSpace π H] {c : E β ContinuousMultilinearMap π M H} (hc : Differentiable π c) (u : (i : ΞΉ) β M i) :
Differentiable π fun (y : E) => (c y) u
theorem fderivWithin_continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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
theorem fderiv_continuousMultilinear_apply_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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
theorem fderivWithin_continuousMultilinear_apply_const_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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.

theorem fderiv_continuousMultilinear_apply_const_apply {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β Type u_7} [(i : ΞΉ) β NormedAddCommGroup (M i)] [(i : ΞΉ) β NormedSpace π (M i)] {H : Type u_8} [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.

theorem HasStrictFDerivAt.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : ) (hf : ) :
HasStrictFDerivAt (fun (y : E) => c y β’ f y) (c x β’ f' + c'.smulRight (f x)) x
theorem HasFDerivWithinAt.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (y : E) => c y β’ f y) (c x β’ f' + c'.smulRight (f x)) s x
theorem HasFDerivAt.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {f' : E βL[π] F} {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (y : E) => c y β’ f y) (c x β’ f' + c'.smulRight (f x)) x
theorem DifferentiableWithinAt.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} {π' : Type u_6} [] [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
@[simp]
theorem DifferentiableAt.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : DifferentiableAt π c x) (hf : DifferentiableAt π f x) :
DifferentiableAt π (fun (y : E) => c y β’ f y) x
theorem DifferentiableOn.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : DifferentiableOn π c s) (hf : DifferentiableOn π f s) :
DifferentiableOn π (fun (y : E) => c y β’ f y) s
@[simp]
theorem Differentiable.smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : Differentiable π c) (hf : Differentiable π f) :
Differentiable π fun (y : E) => c y β’ f y
theorem fderivWithin_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hxs : UniqueDiffWithinAt π s x) (hc : DifferentiableWithinAt π c s x) (hf : DifferentiableWithinAt π f s x) :
fderivWithin π (fun (y : E) => c y β’ f y) s x = c x β’ fderivWithin π f s x + (fderivWithin π c s x).smulRight (f x)
theorem fderiv_smul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {f : E β F} {x : E} {π' : Type u_6} [] [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)
theorem HasStrictFDerivAt.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : ) (f : F) :
HasStrictFDerivAt (fun (y : E) => c y β’ f) (c'.smulRight f) x
theorem HasFDerivWithinAt.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : HasFDerivWithinAt c c' s x) (f : F) :
HasFDerivWithinAt (fun (y : E) => c y β’ f) (c'.smulRight f) s x
theorem HasFDerivAt.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} {c' : E βL[π] π'} (hc : HasFDerivAt c c' x) (f : F) :
HasFDerivAt (fun (y : E) => c y β’ f) (c'.smulRight f) x
theorem DifferentiableWithinAt.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : DifferentiableWithinAt π c s x) (f : F) :
DifferentiableWithinAt π (fun (y : E) => c y β’ f) s x
theorem DifferentiableAt.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : DifferentiableAt π c x) (f : F) :
DifferentiableAt π (fun (y : E) => c y β’ f) x
theorem DifferentiableOn.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {s : Set E} {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : DifferentiableOn π c s) (f : F) :
DifferentiableOn π (fun (y : E) => c y β’ f) s
theorem Differentiable.smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {π' : Type u_6} [] [NormedAlgebra π π'] [NormedSpace π' F] [IsScalarTower π π' F] {c : E β π'} (hc : Differentiable π c) (f : F) :
Differentiable π fun (y : E) => c y β’ f
theorem fderivWithin_smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {s : Set E} {π' : Type u_6} [] [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
theorem fderiv_smul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {x : E} {π' : Type u_6} [] [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 #

theorem HasStrictFDerivAt.mul' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {b : E β πΈ} {a' : E βL[π] πΈ} {b' : E βL[π] πΈ} {x : E} (ha : ) (hb : ) :
HasStrictFDerivAt (fun (y : E) => a y * b y) (a x β’ b' + a'.smulRight (b x)) x
theorem HasStrictFDerivAt.mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ' : Type u_7} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {c : E β πΈ'} {d : E β πΈ'} {c' : E βL[π] πΈ'} {d' : E βL[π] πΈ'} (hc : ) (hd : ) :
HasStrictFDerivAt (fun (y : E) => c y * d y) (c x β’ d' + d x β’ c') x
theorem HasFDerivWithinAt.mul' {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b y) (a x β’ b' + a'.smulRight (b x)) s x
theorem HasFDerivWithinAt.mul {π : Type u_1} [] {E : Type u_2} [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 : E) => c y * d y) (c x β’ d' + d x β’ c') s x
theorem HasFDerivAt.mul' {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b y) (a x β’ b' + a'.smulRight (b x)) x
theorem HasFDerivAt.mul {π : Type u_1} [] {E : Type u_2} [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 : E) => c y * d y) (c x β’ d' + d x β’ c') x
theorem DifferentiableWithinAt.mul {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b y) s x
@[simp]
theorem DifferentiableAt.mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {b : E β πΈ} (ha : DifferentiableAt π a x) (hb : DifferentiableAt π b x) :
DifferentiableAt π (fun (y : E) => a y * b y) x
theorem DifferentiableOn.mul {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b y) s
@[simp]
theorem Differentiable.mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {b : E β πΈ} (ha : Differentiable π a) (hb : Differentiable π b) :
Differentiable π fun (y : E) => a y * b y
theorem DifferentiableWithinAt.pow {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableWithinAt π a s x) (n : β) :
DifferentiableWithinAt π (fun (x : E) => a x ^ n) s x
@[simp]
theorem DifferentiableAt.pow {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableAt π a x) (n : β) :
DifferentiableAt π (fun (x : E) => a x ^ n) x
theorem DifferentiableOn.pow {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableOn π a s) (n : β) :
DifferentiableOn π (fun (x : E) => a x ^ n) s
@[simp]
theorem Differentiable.pow {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : Differentiable π a) (n : β) :
Differentiable π fun (x : E) => a x ^ n
theorem fderivWithin_mul' {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b y) s x = a x β’ fderivWithin π b s x + (fderivWithin π a s x).smulRight (b x)
theorem fderivWithin_mul {π : Type u_1} [] {E : Type u_2} [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 : E) => c y * d y) s x = c x β’ fderivWithin π d s x + d x β’ fderivWithin π c s x
theorem fderiv_mul' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {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)
theorem fderiv_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ' : Type u_7} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {c : E β πΈ'} {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
theorem HasStrictFDerivAt.mul_const' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {a' : E βL[π] πΈ} (ha : ) (b : πΈ) :
HasStrictFDerivAt (fun (y : E) => a y * b) (a'.smulRight b) x
theorem HasStrictFDerivAt.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ' : Type u_7} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {c : E β πΈ'} {c' : E βL[π] πΈ'} (hc : ) (d : πΈ') :
HasStrictFDerivAt (fun (y : E) => c y * d) (d β’ c') x
theorem HasFDerivWithinAt.mul_const' {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b) (a'.smulRight b) s x
theorem HasFDerivWithinAt.mul_const {π : Type u_1} [] {E : Type u_2} [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 : E) => c y * d) (d β’ c') s x
theorem HasFDerivAt.mul_const' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {a' : E βL[π] πΈ} (ha : HasFDerivAt a a' x) (b : πΈ) :
HasFDerivAt (fun (y : E) => a y * b) (a'.smulRight b) x
theorem HasFDerivAt.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ' : Type u_7} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {c : E β πΈ'} {c' : E βL[π] πΈ'} (hc : HasFDerivAt c c' x) (d : πΈ') :
HasFDerivAt (fun (y : E) => c y * d) (d β’ c') x
theorem DifferentiableWithinAt.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableWithinAt π a s x) (b : πΈ) :
DifferentiableWithinAt π (fun (y : E) => a y * b) s x
theorem DifferentiableAt.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableAt π a x) (b : πΈ) :
DifferentiableAt π (fun (y : E) => a y * b) x
theorem DifferentiableOn.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableOn π a s) (b : πΈ) :
DifferentiableOn π (fun (y : E) => a y * b) s
theorem Differentiable.mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : Differentiable π a) (b : πΈ) :
Differentiable π fun (y : E) => a y * b
theorem fderivWithin_mul_const' {π : Type u_1} [] {E : Type u_2} [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 : E) => a y * b) s x = (fderivWithin π a s x).smulRight b
theorem fderivWithin_mul_const {π : Type u_1} [] {E : Type u_2} [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 : E) => c y * d) s x = d β’ fderivWithin π c s x
theorem fderiv_mul_const' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableAt π a x) (b : πΈ) :
fderiv π (fun (y : E) => a y * b) x = (fderiv π a x).smulRight b
theorem fderiv_mul_const {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ' : Type u_7} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {c : E β πΈ'} (hc : DifferentiableAt π c x) (d : πΈ') :
fderiv π (fun (y : E) => c y * d) x = d β’ fderiv π c x
theorem HasStrictFDerivAt.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {a' : E βL[π] πΈ} (ha : ) (b : πΈ) :
HasStrictFDerivAt (fun (y : E) => b * a y) (b β’ a') x
theorem HasFDerivWithinAt.const_mul {π : Type u_1} [] {E : Type u_2} [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 : E) => b * a y) (b β’ a') s x
theorem HasFDerivAt.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} {a' : E βL[π] πΈ} (ha : HasFDerivAt a a' x) (b : πΈ) :
HasFDerivAt (fun (y : E) => b * a y) (b β’ a') x
theorem DifferentiableWithinAt.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableWithinAt π a s x) (b : πΈ) :
DifferentiableWithinAt π (fun (y : E) => b * a y) s x
theorem DifferentiableAt.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableAt π a x) (b : πΈ) :
DifferentiableAt π (fun (y : E) => b * a y) x
theorem DifferentiableOn.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : DifferentiableOn π a s) (b : πΈ) :
DifferentiableOn π (fun (y : E) => b * a y) s
theorem Differentiable.const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {πΈ : Type u_6} [NormedRing πΈ] [NormedAlgebra π πΈ] {a : E β πΈ} (ha : Differentiable π a) (b : πΈ) :
Differentiable π fun (y : E) => b * a y
theorem fderivWithin_const_mul {π : Type u_1} [] {E : Type u_2} [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 : E) => b * a y) s x = b β’ fderivWithin π a s x
theorem fderiv_const_mul {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {x : E} {πΈ : Type u_6} [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 #

theorem hasStrictFDerivAt_list_prod' {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get i)).smulRight (List.map x (List.drop (βi).succ l)).prod) x
theorem hasStrictFDerivAt_list_prod_finRange' {π : Type u_1} [] {πΈ : Type u_7} [NormedRing πΈ] [NormedAlgebra π πΈ] {n : β} {x : Fin n β πΈ} :
HasStrictFDerivAt (fun (x : Fin n β πΈ) => ().prod) (β i : Fin n, (List.map x (List.take (βi) ())).prod β’ .smulRight (List.map x (List.drop (βi).succ ())).prod) x
theorem hasStrictFDerivAt_list_prod_attach' {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ : Type u_7} [NormedRing πΈ] [NormedAlgebra π πΈ] [] {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.get (Fin.cast β― i))).smulRight (List.map x (List.drop (βi).succ l.attach)).prod) x
theorem hasFDerivAt_list_prod' {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [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.get i)).smulRight (List.map x (List.drop (βi).succ l)).prod) x
theorem hasFDerivAt_list_prod_finRange' {π : Type u_1} [] {πΈ : Type u_7} [NormedRing πΈ] [NormedAlgebra π πΈ] {n : β} {x : Fin n β πΈ} :
HasFDerivAt (fun (x : Fin n β πΈ) => ().prod) (β i : Fin n, (List.map x (List.take (βi) ())).prod β’ .smulRight (List.map x (List.drop (βi).succ ())).prod) x
theorem hasFDerivAt_list_prod_attach' {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ : Type u_7} [NormedRing πΈ] [NormedAlgebra π πΈ] [] {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.get (Fin.cast β― i))).smulRight (List.map x (List.drop (βi).succ l.attach)).prod) x
theorem hasStrictFDerivAt_list_prod {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] [] [Fintype ΞΉ] {l : List ΞΉ} {x : ΞΉ β πΈ'} :
HasStrictFDerivAt (fun (x : ΞΉ β πΈ') => (List.map x l).prod) (List.map (fun (i : ΞΉ) => (List.map x (l.erase i)).prod β’ ) l).sum x

Auxiliary lemma for hasStrictFDerivAt_multiset_prod.

For NormedCommRing πΈ', can rewrite as Multiset using Multiset.prod_coe.

theorem hasStrictFDerivAt_multiset_prod {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] [] [Fintype ΞΉ] {u : Multiset ΞΉ} {x : ΞΉ β πΈ'} :
HasStrictFDerivAt (fun (x : ΞΉ β πΈ') => ().prod) (Multiset.map (fun (i : ΞΉ) => (Multiset.map x (u.erase i)).prod β’ ) u).sum x
theorem hasFDerivAt_multiset_prod {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] [] [Fintype ΞΉ] {u : Multiset ΞΉ} {x : ΞΉ β πΈ'} :
HasFDerivAt (fun (x : ΞΉ β πΈ') => ().prod) (Multiset.map (fun (i : ΞΉ) => (Multiset.map x (u.erase i)).prod β’ ) u).sum x
theorem hasStrictFDerivAt_finset_prod {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} [] [Fintype ΞΉ] {x : ΞΉ β πΈ'} :
HasStrictFDerivAt (fun (x : ΞΉ β πΈ') => β i β u, x i) (β i β u, (β j β u.erase i, x j) β’ ) x
theorem hasFDerivAt_finset_prod {π : Type u_1} [] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} [] [Fintype ΞΉ] {x : ΞΉ β πΈ'} :
HasFDerivAt (fun (x : ΞΉ β πΈ') => β i β u, x i) (β i β u, (β j β u.erase i, x j) β’ ) x
theorem HasStrictFDerivAt.list_prod' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get i)).smulRight (List.map (fun (x_1 : ΞΉ) => f x_1 x) (List.drop (βi).succ l)).prod) x
theorem HasFDerivAt.list_prod' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get 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.

theorem HasFDerivWithinAt.list_prod' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get i)).smulRight (List.map (fun (x_1 : ΞΉ) => f x_1 x) (List.drop (βi).succ l)).prod) s x
theorem fderiv_list_prod' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get i) x) x).smulRight (List.map (fun (x_1 : ΞΉ) => f x_1 x) (List.drop (βi).succ l)).prod
theorem fderivWithin_list_prod' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ : Type u_7} [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.get i) x) s x).smulRight (List.map (fun (x_1 : ΞΉ) => f x_1 x) (List.drop (βi).succ l)).prod
theorem HasStrictFDerivAt.multiset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {u : Multiset ΞΉ} {x : E} (h : β i β u, HasStrictFDerivAt (fun (x : E) => g i x) (g' i) x) :
HasStrictFDerivAt (fun (x : E) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) u).prod) (Multiset.map (fun (i : ΞΉ) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) (u.erase i)).prod β’ g' i) u).sum x
theorem HasFDerivAt.multiset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {u : Multiset ΞΉ} {x : E} (h : β i β u, HasFDerivAt (fun (x : E) => g i x) (g' i) x) :
HasFDerivAt (fun (x : E) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) u).prod) (Multiset.map (fun (i : ΞΉ) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) (u.erase i)).prod β’ g' i) u).sum x

Unlike HasFDerivAt.finset_prod, supports duplicate elements.

theorem HasFDerivWithinAt.multiset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {u : Multiset ΞΉ} {x : E} (h : β i β u, HasFDerivWithinAt (fun (x : E) => g i x) (g' i) s x) :
HasFDerivWithinAt (fun (x : E) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) u).prod) (Multiset.map (fun (i : ΞΉ) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) (u.erase i)).prod β’ g' i) u).sum s x
theorem fderiv_multiset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {g : ΞΉ β E β πΈ'} [] {u : Multiset ΞΉ} {x : E} (h : β i β u, DifferentiableAt π (fun (x : E) => g i x) x) :
fderiv π (fun (x : E) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) u).prod) x = (Multiset.map (fun (i : ΞΉ) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) (u.erase i)).prod β’ fderiv π (g i) x) u).sum
theorem fderivWithin_multiset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {g : ΞΉ β E β πΈ'} [] {u : Multiset ΞΉ} {x : E} (hxs : UniqueDiffWithinAt π s x) (h : β i β u, DifferentiableWithinAt π (fun (x : E) => g i x) s x) :
fderivWithin π (fun (x : E) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) u).prod) s x = (Multiset.map (fun (i : ΞΉ) => (Multiset.map (fun (x_1 : ΞΉ) => g x_1 x) (u.erase i)).prod β’ fderivWithin π (g i) s x) u).sum
theorem HasStrictFDerivAt.finset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {x : E} (hg : β i β u, HasStrictFDerivAt (g i) (g' i) x) :
HasStrictFDerivAt (fun (x : E) => β i β u, g i x) (β i β u, (β j β u.erase i, g j x) β’ g' i) x
theorem HasFDerivAt.finset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {x : E} (hg : β i β u, HasFDerivAt (g i) (g' i) x) :
HasFDerivAt (fun (x : E) => β i β u, g i x) (β i β u, (β j β u.erase i, g j x) β’ g' i) x
theorem HasFDerivWithinAt.finset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} {g : ΞΉ β E β πΈ'} {g' : ΞΉ β E βL[π] πΈ'} [] {x : E} (hg : β i β u, HasFDerivWithinAt (g i) (g' i) s x) :
HasFDerivWithinAt (fun (x : E) => β i β u, g i x) (β i β u, (β j β u.erase i, g j x) β’ g' i) s x
theorem fderiv_finset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} {g : ΞΉ β E β πΈ'} [] {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
theorem fderivWithin_finset_prod {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {s : Set E} {ΞΉ : Type u_6} {πΈ' : Type u_8} [NormedCommRing πΈ'] [NormedAlgebra π πΈ'] {u : Finset ΞΉ} {g : ΞΉ β E β πΈ'} [] {x : E} (hxs : UniqueDiffWithinAt π s x) (hg : β i β u, DifferentiableWithinAt π (g i) s x) :
fderivWithin π (fun (x : E) => β i β u, g i x) s x = β i β u, (β j β u.erase i, g j x) β’ fderivWithin π (g i) s x
theorem hasFDerivAt_ring_inverse {π : Type u_1} [] {R : Type u_6} [] [NormedAlgebra π R] [] (x : RΛ£) :
HasFDerivAt Ring.inverse (-(() β) β) β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.

theorem differentiableAt_inverse {π : Type u_1} [] {R : Type u_6} [] [NormedAlgebra π R] [] {x : R} (hx : ) :
DifferentiableAt π Ring.inverse x
theorem differentiableWithinAt_inverse {π : Type u_1} [] {R : Type u_6} [] [NormedAlgebra π R] [] {x : R} (hx : ) (s : Set R) :
DifferentiableWithinAt π Ring.inverse s x
theorem differentiableOn_inverse {π : Type u_1} [] {R : Type u_6} [] [NormedAlgebra π R] [] :
DifferentiableOn π Ring.inverse {x : R | }
theorem fderiv_inverse {π : Type u_1} [] {R : Type u_6} [] [NormedAlgebra π R] [] (x : RΛ£) :
fderiv π Ring.inverse βx = -(() β) β
theorem DifferentiableWithinAt.inverse {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [] [NormedAlgebra π R] [] {h : E β R} {z : E} {S : Set E} (hf : DifferentiableWithinAt π h S z) (hz : IsUnit (h z)) :
DifferentiableWithinAt π (fun (x : E) => Ring.inverse (h x)) S z
@[simp]
theorem DifferentiableAt.inverse {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [] [NormedAlgebra π R] [] {h : E β R} {z : E} (hf : DifferentiableAt π h z) (hz : IsUnit (h z)) :
DifferentiableAt π (fun (x : E) => Ring.inverse (h x)) z
theorem DifferentiableOn.inverse {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [] [NormedAlgebra π R] [] {h : E β R} {S : Set E} (hf : DifferentiableOn π h S) (hz : β x β S, IsUnit (h x)) :
DifferentiableOn π (fun (x : E) => Ring.inverse (h x)) S
@[simp]
theorem Differentiable.inverse {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [] [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 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.

theorem hasFDerivAt_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] {x : R} (hx : x β  0) :
HasFDerivAt Inv.inv (-(() ) ) 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β»ΒΉ.

theorem differentiableAt_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] {x : R} (hx : x β  0) :
DifferentiableAt π Inv.inv x
theorem differentiableWithinAt_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] {x : R} (hx : x β  0) (s : Set R) :
DifferentiableWithinAt π (fun (x : R) => ) s x
theorem differentiableOn_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] :
DifferentiableOn π (fun (x : R) => ) {x : R | x β  0}
theorem fderiv_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] {x : R} (hx : x β  0) :
fderiv π Inv.inv x = -(() )

Non-commutative version of fderiv_inv

theorem fderivWithin_inv' {π : Type u_1} [] {R : Type u_6} [NormedAlgebra π R] [] {s : Set R} {x : R} (hx : x β  0) (hxs : UniqueDiffWithinAt π s x) :
fderivWithin π (fun (x : R) => ) s x = -(() )

Non-commutative version of fderivWithin_inv

theorem DifferentiableWithinAt.inv' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [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
@[simp]
theorem DifferentiableAt.inv' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [NormedAlgebra π R] [] {h : E β R} {z : E} (hf : DifferentiableAt π h z) (hz : h z β  0) :
DifferentiableAt π (fun (x : E) => (h x)β»ΒΉ) z
theorem DifferentiableOn.inv' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [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
@[simp]
theorem Differentiable.inv' {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {R : Type u_6} [NormedAlgebra π R] [] {h : E β R} (hf : Differentiable π h) (hz : β (x : E), h x β  0) :
Differentiable π fun (x : E) => (h x)β»ΒΉ