The derivative of bounded bilinear maps

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 bounded bilinear maps.

Derivative of a bounded bilinear map

theorem IsBoundedBilinearMap.hasStrictFDerivAt {𝕜 : 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] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasStrictFDerivAt b (h.deriv p) p

theorem IsBoundedBilinearMap.hasFDerivAt {𝕜 : 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] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasFDerivAt b (h.deriv p) p

theorem IsBoundedBilinearMap.hasFDerivWithinAt {𝕜 : 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] {b : E × F → G} {u : Set (E × F)} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : HasFDerivWithinAt b (h.deriv p) u p

theorem IsBoundedBilinearMap.differentiableAt {𝕜 : 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] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableAt 𝕜 b p

theorem IsBoundedBilinearMap.differentiableWithinAt {𝕜 : 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] {b : E × F → G} {u : Set (E × F)} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : DifferentiableWithinAt 𝕜 b u p

theorem IsBoundedBilinearMap.fderiv {𝕜 : 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] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) : fderiv 𝕜 b p = h.deriv p

theorem IsBoundedBilinearMap.fderivWithin {𝕜 : 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] {b : E × F → G} {u : Set (E × F)} (h : IsBoundedBilinearMap 𝕜 b) (p : E × F) (hxs : UniqueDiffWithinAt 𝕜 u p) : fderivWithin 𝕜 b u p = h.deriv p

theorem IsBoundedBilinearMap.differentiable {𝕜 : 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] {b : E × F → G} (h : IsBoundedBilinearMap 𝕜 b) : Differentiable 𝕜 b

theorem IsBoundedBilinearMap.differentiableOn {𝕜 : 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] {b : E × F → G} {u : Set (E × F)} (h : IsBoundedBilinearMap 𝕜 b) : DifferentiableOn 𝕜 b u

theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {𝕜 : 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] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} {s : Set G'} (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) : HasFDerivWithinAt (fun (y : G') => (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) s x

theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {𝕜 : 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] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x) : HasFDerivAt (fun (y : G') => (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) x

theorem ContinuousLinearMap.hasStrictFDerivAt_of_bilinear {𝕜 : 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] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun (y : G') => (B (f y)) (g y)) (((precompR G' B) (f x)) g' + ((precompL G' B) f') (g x)) x

theorem ContinuousLinearMap.fderivWithin_of_bilinear {𝕜 : 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] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {x : G'} {s : Set G'} (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) (hs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 (fun (y : G') => (B (f y)) (g y)) s x = ((precompR G' B) (f x)) (fderivWithin 𝕜 g s x) + ((precompL G' B) (fderivWithin 𝕜 f s x)) (g x)

theorem ContinuousLinearMap.fderiv_of_bilinear {𝕜 : 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] {G' : Type u_5} [NormedAddCommGroup G'] [NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {x : G'} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : fderiv 𝕜 (fun (y : G') => (B (f y)) (g y)) x = ((precompR G' B) (f x)) (fderiv 𝕜 g x) + ((precompL G' B) (fderiv 𝕜 f x)) (g x)