# The derivative of bounded bilinear maps #

For detailed documentation of the FrΓ©chet derivative, see the module docstring of 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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} (h : IsBoundedBilinearMap π b) (p : E Γ F) :
HasStrictFDerivAt b (h.deriv p) p
theorem IsBoundedBilinearMap.hasFDerivAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} (h : IsBoundedBilinearMap π b) (p : E Γ F) :
HasFDerivAt b (h.deriv p) p
theorem IsBoundedBilinearMap.hasFDerivWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} (h : IsBoundedBilinearMap π b) (p : E Γ F) :
DifferentiableAt π b p
theorem IsBoundedBilinearMap.differentiableWithinAt {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} (h : IsBoundedBilinearMap π b) (p : E Γ F) :
fderiv π b p = h.deriv p
theorem IsBoundedBilinearMap.fderivWithin {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [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} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} (h : IsBoundedBilinearMap π b) :
Differentiable π b
theorem IsBoundedBilinearMap.differentiableOn {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {b : E Γ F β G} {u : Set (E Γ F)} (h : IsBoundedBilinearMap π b) :
DifferentiableOn π b u
theorem ContinuousLinearMap.hasFDerivWithinAt_of_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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)) (( (f x)) g' + ( f') (g x)) s x
theorem ContinuousLinearMap.hasFDerivAt_of_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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)) (( (f x)) g' + ( f') (g x)) x
theorem ContinuousLinearMap.hasStrictFDerivAt_of_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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 : ) (hg : ) :
HasStrictFDerivAt (fun (y : G') => (B (f y)) (g y)) (( (f x)) g' + ( f') (g x)) x
theorem ContinuousLinearMap.fderivWithin_of_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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 = ( (f x)) (fderivWithin π g s x) + ( (fderivWithin π f s x)) (g x)
theorem ContinuousLinearMap.fderiv_of_bilinear {π : Type u_1} [] {E : Type u_2} [NormedSpace π E] {F : Type u_3} [NormedSpace π F] {G : Type u_4} [NormedSpace π G] {G' : Type u_5} [] [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 = ( (f x)) (fderiv π g x) + ( (fderiv π f x)) (g x)