Documentation

Mathlib.Analysis.Calculus.FDeriv.Bilinear

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} [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)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.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)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.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)) (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.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 = ((ContinuousLinearMap.precompR G' B) (f x)) (fderivWithin π•œ g s x) + ((ContinuousLinearMap.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 = ((ContinuousLinearMap.precompR G' B) (f x)) (fderiv π•œ g x) + ((ContinuousLinearMap.precompL G' B) (fderiv π•œ f x)) (g x)