Documentation

Mathlib.Analysis.Calculus.FDeriv.Mul

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

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

source
theorem HasStrictFDerivAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
HasStrictFDerivAt (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp ((ContinuousLinearMap.compL π•œ F G H) (c x)) d' + ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL π•œ F G H)) (d x)) c') x
source
theorem HasFDerivWithinAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
HasFDerivWithinAt (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp ((ContinuousLinearMap.compL π•œ F G H) (c x)) d' + ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL π•œ F G H)) (d x)) c') s x
source
theorem HasFDerivAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
HasFDerivAt (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) (ContinuousLinearMap.comp ((ContinuousLinearMap.compL π•œ F G H) (c x)) d' + ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL π•œ F G H)) (d x)) c') x
source
theorem DifferentiableWithinAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableWithinAt π•œ c s x) (hd : DifferentiableWithinAt π•œ d s x) :
DifferentiableWithinAt π•œ (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) s x
source
theorem DifferentiableAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
DifferentiableAt π•œ (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) x
source
theorem DifferentiableOn.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableOn π•œ c s) (hd : DifferentiableOn π•œ d s) :
DifferentiableOn π•œ (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) s
source
theorem Differentiable.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : Differentiable π•œ c) (hd : Differentiable π•œ d) :
Differentiable π•œ fun (y : E) => ContinuousLinearMap.comp (c y) (d y)
source
theorem fderivWithin_clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hd : DifferentiableWithinAt π•œ d s x) :
fderivWithin π•œ (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) s x = ContinuousLinearMap.comp ((ContinuousLinearMap.compL π•œ F G H) (c x)) (fderivWithin π•œ d s x) + ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL π•œ F G H)) (d x)) (fderivWithin π•œ c s x)
source
theorem fderiv_clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
fderiv π•œ (fun (y : E) => ContinuousLinearMap.comp (c y) (d y)) x = ContinuousLinearMap.comp ((ContinuousLinearMap.compL π•œ F G H) (c x)) (fderiv π•œ d x) + ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL π•œ F G H)) (d x)) (fderiv π•œ c x)
source
theorem HasStrictFDerivAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasStrictFDerivAt c c' x) (hu : HasStrictFDerivAt u u' x) :
HasStrictFDerivAt (fun (y : E) => (c y) (u y)) (ContinuousLinearMap.comp (c x) u' + (ContinuousLinearMap.flip c') (u x)) x
source
theorem HasFDerivWithinAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) :
HasFDerivWithinAt (fun (y : E) => (c y) (u y)) (ContinuousLinearMap.comp (c x) u' + (ContinuousLinearMap.flip c') (u x)) s x
source
theorem HasFDerivAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
HasFDerivAt (fun (y : E) => (c y) (u y)) (ContinuousLinearMap.comp (c x) u' + (ContinuousLinearMap.flip c') (u x)) x
source
theorem DifferentiableWithinAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableWithinAt π•œ c s x) (hu : DifferentiableWithinAt π•œ u s x) :
DifferentiableWithinAt π•œ (fun (y : 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_6} [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_6} [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_6} [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_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hu : DifferentiableWithinAt π•œ u s x) :
fderivWithin π•œ (fun (y : E) => (c y) (u y)) s x = ContinuousLinearMap.comp (c x) (fderivWithin π•œ u s x) + (ContinuousLinearMap.flip (fderivWithin π•œ c s x)) (u x)
source
theorem fderiv_clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_6} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableAt π•œ c x) (hu : DifferentiableAt π•œ u x) :
fderiv π•œ (fun (y : E) => (c y) (u y)) x = ContinuousLinearMap.comp (c x) (fderiv π•œ u x) + (ContinuousLinearMap.flip (fderiv π•œ c x)) (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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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) ((ContinuousLinearMap.flipMultilinear c') 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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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) ((ContinuousLinearMap.flipMultilinear c') 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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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) ((ContinuousLinearMap.flipMultilinear c') 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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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 = (ContinuousLinearMap.flipMultilinear (fderivWithin π•œ c s x)) u
source
theorem fderiv_continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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 = (ContinuousLinearMap.flipMultilinear (fderiv π•œ c x)) 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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_7} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_8} [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_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasStrictFDerivAt c c' x) (hf : HasStrictFDerivAt f f' x) :
HasStrictFDerivAt (fun (y : E) => c y β€’ f y) (c x β€’ f' + ContinuousLinearMap.smulRight c' (f x)) x
source
theorem HasFDerivWithinAt.smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {s : Set E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasFDerivWithinAt c c' s x) (hf : HasFDerivWithinAt f f' s x) :
HasFDerivWithinAt (fun (y : E) => c y β€’ f y) (c x β€’ f' + ContinuousLinearMap.smulRight c' (f x)) s x
source
theorem HasFDerivAt.smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {f' : E β†’L[π•œ] F} {x : E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
HasFDerivAt (fun (y : E) => c y β€’ f y) (c x β€’ f' + ContinuousLinearMap.smulRight c' (f x)) x
source
theorem DifferentiableWithinAt.smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {s : Set E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} (hc : DifferentiableWithinAt π•œ c s x) (hf : DifferentiableWithinAt π•œ f s x) :
DifferentiableWithinAt π•œ (fun (y : 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_6} [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_6} [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_6} [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_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hf : DifferentiableWithinAt π•œ f s x) :
fderivWithin π•œ (fun (y : E) => c y β€’ f y) s x = c x β€’ fderivWithin π•œ f s x + ContinuousLinearMap.smulRight (fderivWithin π•œ c s x) (f x)
source
theorem fderiv_smul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {f : E β†’ F} {x : E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} (hc : DifferentiableAt π•œ c x) (hf : DifferentiableAt π•œ f x) :
fderiv π•œ (fun (y : E) => c y β€’ f y) x = c x β€’ fderiv π•œ f x + ContinuousLinearMap.smulRight (fderiv π•œ c x) (f x)
source
theorem HasStrictFDerivAt.smul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasStrictFDerivAt c c' x) (f : F) :
HasStrictFDerivAt (fun (y : E) => c y β€’ f) (ContinuousLinearMap.smulRight c' f) x
source
theorem HasFDerivWithinAt.smul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {s : Set E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasFDerivWithinAt c c' s x) (f : F) :
HasFDerivWithinAt (fun (y : E) => c y β€’ f) (ContinuousLinearMap.smulRight c' f) s x
source
theorem HasFDerivAt.smul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} {c' : E β†’L[π•œ] π•œ'} (hc : HasFDerivAt c c' x) (f : F) :
HasFDerivAt (fun (y : E) => c y β€’ f) (ContinuousLinearMap.smulRight c' f) x
source
theorem DifferentiableWithinAt.smul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {s : Set E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} (hc : DifferentiableWithinAt π•œ c s x) (f : F) :
DifferentiableWithinAt π•œ (fun (y : 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_6} [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_6} [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_6} [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_6} [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 = ContinuousLinearMap.smulRight (fderivWithin π•œ c s x) f
source
theorem fderiv_smul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {x : E} {π•œ' : Type u_6} [NontriviallyNormedField π•œ'] [NormedAlgebra π•œ π•œ'] [NormedSpace π•œ' F] [IsScalarTower π•œ π•œ' F] {c : E β†’ π•œ'} (hc : DifferentiableAt π•œ c x) (f : F) :
fderiv π•œ (fun (y : E) => c y β€’ f) x = ContinuousLinearMap.smulRight (fderiv π•œ c x) f

Derivative of the product of two functions #

source
theorem HasStrictFDerivAt.mul' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {b : E β†’ 𝔸} {a' : E β†’L[π•œ] 𝔸} {b' : E β†’L[π•œ] 𝔸} {x : E} (ha : HasStrictFDerivAt a a' x) (hb : HasStrictFDerivAt b b' x) :
HasStrictFDerivAt (fun (y : E) => a y * b y) (a x β€’ b' + ContinuousLinearMap.smulRight a' (b x)) x
source
theorem HasStrictFDerivAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {d : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} {d' : E β†’L[π•œ] 𝔸'} (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
HasStrictFDerivAt (fun (y : 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_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' + ContinuousLinearMap.smulRight a' (b x)) s x
source
theorem HasFDerivWithinAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {d : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} {d' : E β†’L[π•œ] 𝔸'} (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
HasFDerivWithinAt (fun (y : 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_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' + ContinuousLinearMap.smulRight a' (b x)) x
source
theorem HasFDerivAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {d : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} {d' : E β†’L[π•œ] 𝔸'} (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
HasFDerivAt (fun (y : 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_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
source
@[simp]
theorem DifferentiableAt.mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {b : E β†’ 𝔸} (ha : DifferentiableAt π•œ a x) (hb : DifferentiableAt π•œ b x) :
DifferentiableAt π•œ (fun (y : 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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {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_6} [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_6} [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_6} [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_6} [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_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 + ContinuousLinearMap.smulRight (fderivWithin π•œ a s x) (b x)
source
theorem fderivWithin_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {d : E β†’ 𝔸'} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hd : DifferentiableWithinAt π•œ d s x) :
fderivWithin π•œ (fun (y : 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_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 + ContinuousLinearMap.smulRight (fderiv π•œ a x) (b x)
source
theorem fderiv_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {d : E β†’ 𝔸'} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
fderiv π•œ (fun (y : 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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {a' : E β†’L[π•œ] 𝔸} (ha : HasStrictFDerivAt a a' x) (b : 𝔸) :
HasStrictFDerivAt (fun (y : E) => a y * b) (ContinuousLinearMap.smulRight a' b) x
source
theorem HasStrictFDerivAt.mul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} (hc : HasStrictFDerivAt c c' x) (d : 𝔸') :
HasStrictFDerivAt (fun (y : 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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {a' : E β†’L[π•œ] 𝔸} (ha : HasFDerivWithinAt a a' s x) (b : 𝔸) :
HasFDerivWithinAt (fun (y : E) => a y * b) (ContinuousLinearMap.smulRight a' b) s x
source
theorem HasFDerivWithinAt.mul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} (hc : HasFDerivWithinAt c c' s x) (d : 𝔸') :
HasFDerivWithinAt (fun (y : 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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {a' : E β†’L[π•œ] 𝔸} (ha : HasFDerivAt a a' x) (b : 𝔸) :
HasFDerivAt (fun (y : E) => a y * b) (ContinuousLinearMap.smulRight a' b) x
source
theorem HasFDerivAt.mul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} {c' : E β†’L[π•œ] 𝔸'} (hc : HasFDerivAt c c' x) (d : 𝔸') :
HasFDerivAt (fun (y : 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_6} [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_6} [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_6} [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_6} [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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} (hxs : UniqueDiffWithinAt π•œ s x) (ha : DifferentiableWithinAt π•œ a s x) (b : 𝔸) :
fderivWithin π•œ (fun (y : E) => a y * b) s x = ContinuousLinearMap.smulRight (fderivWithin π•œ a s x) b
source
theorem fderivWithin_mul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (d : 𝔸') :
fderivWithin π•œ (fun (y : 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_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} (ha : DifferentiableAt π•œ a x) (b : 𝔸) :
fderiv π•œ (fun (y : E) => a y * b) x = ContinuousLinearMap.smulRight (fderiv π•œ a x) b
source
theorem fderiv_mul_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸' : Type u_7} [NormedCommRing 𝔸'] [NormedAlgebra π•œ 𝔸'] {c : E β†’ 𝔸'} (hc : DifferentiableAt π•œ c x) (d : 𝔸') :
fderiv π•œ (fun (y : 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_6} [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_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
source
theorem HasFDerivAt.const_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} {a' : E β†’L[π•œ] 𝔸} (ha : HasFDerivAt a a' x) (b : 𝔸) :
HasFDerivAt (fun (y : 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_6} [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_6} [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_6} [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_6} [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_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
source
theorem fderiv_const_mul {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {𝔸 : Type u_6} [NormedRing 𝔸] [NormedAlgebra π•œ 𝔸] {a : E β†’ 𝔸} (ha : DifferentiableAt π•œ a x) (b : 𝔸) :
fderiv π•œ (fun (y : E) => b * a y) x = b β€’ fderiv π•œ a x
source
theorem hasFDerivAt_ring_inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] (x : RΛ£) :
HasFDerivAt Ring.inverse (-((ContinuousLinearMap.mulLeftRight π•œ R) ↑x⁻¹) ↑x⁻¹) ↑x

At an invertible element x of a normed algebra R, the FrΓ©chet derivative of the inversion operation is the linear map fun t ↦ - x⁻¹ * t * x⁻¹.

TODO: prove that Ring.inverse is analytic and use it to prove a HasStrictFDerivAt lemma. TODO (low prio): prove a version without assumption [CompleteSpace R] but within the set of units.

source
theorem differentiableAt_inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : IsUnit x) :
DifferentiableAt π•œ Ring.inverse x
source
theorem differentiableWithinAt_inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : IsUnit x) (s : Set R) :
DifferentiableWithinAt π•œ Ring.inverse s x
source
theorem differentiableOn_inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] :
DifferentiableOn π•œ Ring.inverse {x : R | IsUnit x}
source
theorem fderiv_inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] (x : RΛ£) :
fderiv π•œ Ring.inverse ↑x = -((ContinuousLinearMap.mulLeftRight π•œ R) ↑x⁻¹) ↑x⁻¹
source
theorem DifferentiableWithinAt.inverse {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {R : Type u_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {h : E β†’ R} {z : E} {S : Set E} (hf : DifferentiableWithinAt π•œ h S z) (hz : IsUnit (h z)) :
DifferentiableWithinAt π•œ (fun (x : 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_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace 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_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace 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_6} [NormedRing R] [NormedAlgebra π•œ R] [CompleteSpace 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.

source
theorem hasFDerivAt_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : x β‰  0) :
HasFDerivAt Inv.inv (-((ContinuousLinearMap.mulLeftRight π•œ R) x⁻¹) x⁻¹) x

At an invertible element x of a normed division algebra R, the Fréchet derivative of the inversion operation is the linear map λ t, - x⁻¹ * t * x⁻¹.

source
theorem differentiableAt_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : x β‰  0) :
DifferentiableAt π•œ Inv.inv x
source
theorem differentiableWithinAt_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : x β‰  0) (s : Set R) :
DifferentiableWithinAt π•œ (fun (x : R) => x⁻¹) s x
source
theorem differentiableOn_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] :
DifferentiableOn π•œ (fun (x : R) => x⁻¹) {x : R | x β‰  0}
source
theorem fderiv_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {x : R} (hx : x β‰  0) :
fderiv π•œ Inv.inv x = -((ContinuousLinearMap.mulLeftRight π•œ R) x⁻¹) x⁻¹

Non-commutative version of fderiv_inv

source
theorem fderivWithin_inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {s : Set R} {x : R} (hx : x β‰  0) (hxs : UniqueDiffWithinAt π•œ s x) :
fderivWithin π•œ (fun (x : 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_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {h : E β†’ R} {z : E} {S : Set E} (hf : DifferentiableWithinAt π•œ h S z) (hz : h z β‰  0) :
DifferentiableWithinAt π•œ (fun (x : E) => (h x)⁻¹) S z
source
@[simp]
theorem DifferentiableAt.inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {h : E β†’ R} {z : E} (hf : DifferentiableAt π•œ h z) (hz : h z β‰  0) :
DifferentiableAt π•œ (fun (x : E) => (h x)⁻¹) z
source
theorem DifferentiableOn.inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {h : E β†’ R} {S : Set E} (hf : DifferentiableOn π•œ h S) (hz : βˆ€ x ∈ S, h x β‰  0) :
DifferentiableOn π•œ (fun (x : E) => (h x)⁻¹) S
source
@[simp]
theorem Differentiable.inv' {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {R : Type u_6} [NormedDivisionRing R] [NormedAlgebra π•œ R] [CompleteSpace R] {h : E β†’ R} (hf : Differentiable π•œ h) (hz : βˆ€ (x : E), h x β‰  0) :
Differentiable π•œ fun (x : E) => (h x)⁻¹