Documentation

Mathlib.Analysis.Calculus.FDeriv.CompCLM

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_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasStrictFDerivAt c c' x) (hd : HasStrictFDerivAt d d' x) :
HasStrictFDerivAt (fun (y : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL π•œ F G H) (c x)).comp d' + ((ContinuousLinearMap.compL π•œ F G H).flip (d x)).comp c') x
source
theorem HasFDerivWithinAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasFDerivWithinAt c c' s x) (hd : HasFDerivWithinAt d d' s x) :
HasFDerivWithinAt (fun (y : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL π•œ F G H) (c x)).comp d' + ((ContinuousLinearMap.compL π•œ F G H).flip (d x)).comp c') s x
source
theorem HasFDerivAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} {d' : E β†’L[π•œ] F β†’L[π•œ] G} (hc : HasFDerivAt c c' x) (hd : HasFDerivAt d d' x) :
HasFDerivAt (fun (y : E) => (c y).comp (d y)) (((ContinuousLinearMap.compL π•œ F G H) (c x)).comp d' + ((ContinuousLinearMap.compL π•œ F G H).flip (d x)).comp c') x
source
theorem DifferentiableWithinAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableWithinAt π•œ c s x) (hd : DifferentiableWithinAt π•œ d s x) :
DifferentiableWithinAt π•œ (fun (y : E) => (c y).comp (d y)) s x
source
theorem DifferentiableAt.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
DifferentiableAt π•œ (fun (y : E) => (c y).comp (d y)) x
source
theorem DifferentiableOn.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableOn π•œ c s) (hd : DifferentiableOn π•œ d s) :
DifferentiableOn π•œ (fun (y : E) => (c y).comp (d y)) s
source
theorem Differentiable.clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : Differentiable π•œ c) (hd : Differentiable π•œ d) :
Differentiable π•œ fun (y : E) => (c y).comp (d y)
source
theorem fderivWithin_clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hd : DifferentiableWithinAt π•œ d s x) :
fderivWithin π•œ (fun (y : E) => (c y).comp (d y)) s x = ((ContinuousLinearMap.compL π•œ F G H) (c x)).comp (fderivWithin π•œ d s x) + ((ContinuousLinearMap.compL π•œ F G H).flip (d x)).comp (fderivWithin π•œ c s x)
source
theorem fderiv_clm_comp {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace π•œ F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {d : E β†’ F β†’L[π•œ] G} (hc : DifferentiableAt π•œ c x) (hd : DifferentiableAt π•œ d x) :
fderiv π•œ (fun (y : E) => (c y).comp (d y)) x = ((ContinuousLinearMap.compL π•œ F G H) (c x)).comp (fderiv π•œ d x) + ((ContinuousLinearMap.compL π•œ F G H).flip (d x)).comp (fderiv π•œ c x)
source
theorem HasStrictFDerivAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasStrictFDerivAt c c' x) (hu : HasStrictFDerivAt u u' x) :
HasStrictFDerivAt (fun (y : E) => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x
source
theorem HasFDerivWithinAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasFDerivWithinAt c c' s x) (hu : HasFDerivWithinAt u u' s x) :
HasFDerivWithinAt (fun (y : E) => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) s x
source
theorem HasFDerivAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {c' : E β†’L[π•œ] G β†’L[π•œ] H} {u : E β†’ G} {u' : E β†’L[π•œ] G} (hc : HasFDerivAt c c' x) (hu : HasFDerivAt u u' x) :
HasFDerivAt (fun (y : E) => (c y) (u y)) ((c x).comp u' + c'.flip (u x)) x
source
theorem DifferentiableWithinAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableWithinAt π•œ c s x) (hu : DifferentiableWithinAt π•œ u s x) :
DifferentiableWithinAt π•œ (fun (y : E) => (c y) (u y)) s x
source
theorem DifferentiableAt.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableAt π•œ c x) (hu : DifferentiableAt π•œ u x) :
DifferentiableAt π•œ (fun (y : E) => (c y) (u y)) x
source
theorem DifferentiableOn.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableOn π•œ c s) (hu : DifferentiableOn π•œ u s) :
DifferentiableOn π•œ (fun (y : E) => (c y) (u y)) s
source
theorem Differentiable.clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : Differentiable π•œ c) (hu : Differentiable π•œ u) :
Differentiable π•œ fun (y : E) => (c y) (u y)
source
theorem fderivWithin_clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {s : Set E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (hu : DifferentiableWithinAt π•œ u s x) :
fderivWithin π•œ (fun (y : E) => (c y) (u y)) s x = (c x).comp (fderivWithin π•œ u s x) + (fderivWithin π•œ c s x).flip (u x)
source
theorem fderiv_clm_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace π•œ G] {x : E} {H : Type u_5} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ G β†’L[π•œ] H} {u : E β†’ G} (hc : DifferentiableAt π•œ c x) (hu : DifferentiableAt π•œ u x) :
fderiv π•œ (fun (y : E) => (c y) (u y)) x = (c x).comp (fderiv π•œ u x) + (fderiv π•œ c x).flip (u x)

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

source
theorem HasStrictFDerivAt.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} {c' : E β†’L[π•œ] ContinuousMultilinearMap π•œ M H} (hc : HasStrictFDerivAt c c' x) (u : (i : ΞΉ) β†’ M i) :
HasStrictFDerivAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) x
source
theorem HasFDerivWithinAt.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} {c' : E β†’L[π•œ] ContinuousMultilinearMap π•œ M H} (hc : HasFDerivWithinAt c c' s x) (u : (i : ΞΉ) β†’ M i) :
HasFDerivWithinAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) s x
source
theorem HasFDerivAt.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} {c' : E β†’L[π•œ] ContinuousMultilinearMap π•œ M H} (hc : HasFDerivAt c c' x) (u : (i : ΞΉ) β†’ M i) :
HasFDerivAt (fun (y : E) => (c y) u) (c'.flipMultilinear u) x
source
theorem DifferentiableWithinAt.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : DifferentiableWithinAt π•œ c s x) (u : (i : ΞΉ) β†’ M i) :
DifferentiableWithinAt π•œ (fun (y : E) => (c y) u) s x
source
theorem DifferentiableAt.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : DifferentiableAt π•œ c x) (u : (i : ΞΉ) β†’ M i) :
DifferentiableAt π•œ (fun (y : E) => (c y) u) x
source
theorem DifferentiableOn.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {s : Set E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : DifferentiableOn π•œ c s) (u : (i : ΞΉ) β†’ M i) :
DifferentiableOn π•œ (fun (y : E) => (c y) u) s
source
theorem Differentiable.continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : Differentiable π•œ c) (u : (i : ΞΉ) β†’ M i) :
Differentiable π•œ fun (y : E) => (c y) u
source
theorem fderivWithin_continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (u : (i : ΞΉ) β†’ M i) :
fderivWithin π•œ (fun (y : E) => (c y) u) s x = (fderivWithin π•œ c s x).flipMultilinear u
source
theorem fderiv_continuousMultilinear_apply_const {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : DifferentiableAt π•œ c x) (u : (i : ΞΉ) β†’ M i) :
fderiv π•œ (fun (y : E) => (c y) u) x = (fderiv π•œ c x).flipMultilinear u
source
theorem fderivWithin_continuousMultilinear_apply_const_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {s : Set E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hxs : UniqueDiffWithinAt π•œ s x) (hc : DifferentiableWithinAt π•œ c s x) (u : (i : ΞΉ) β†’ M i) (m : E) :
(fderivWithin π•œ (fun (y : E) => (c y) u) s x) m = ((fderivWithin π•œ c s x) m) u

Application of a ContinuousMultilinearMap to a constant commutes with fderivWithin.

source
theorem fderiv_continuousMultilinear_apply_const_apply {π•œ : Type u_1} [NontriviallyNormedField π•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace π•œ E] {x : E} {ΞΉ : Type u_5} [Fintype ΞΉ] {M : ΞΉ β†’ Type u_6} [(i : ΞΉ) β†’ NormedAddCommGroup (M i)] [(i : ΞΉ) β†’ NormedSpace π•œ (M i)] {H : Type u_7} [NormedAddCommGroup H] [NormedSpace π•œ H] {c : E β†’ ContinuousMultilinearMap π•œ M H} (hc : DifferentiableAt π•œ c x) (u : (i : ΞΉ) β†’ M i) (m : E) :
(fderiv π•œ (fun (y : E) => (c y) u) x) m = ((fderiv π•œ c x) m) u

Application of a ContinuousMultilinearMap to a constant commutes with fderiv.