mathlib3 documentation

analysis.calculus.fderiv.bilinear

The derivative of bounded bilinear maps #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 is_bounded_bilinear_map.has_strict_fderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
theorem is_bounded_bilinear_map.has_fderiv_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
theorem is_bounded_bilinear_map.has_fderiv_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} {u : set (E × F)} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
theorem is_bounded_bilinear_map.differentiable_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
theorem is_bounded_bilinear_map.differentiable_within_at {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} {u : set (E × F)} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
theorem is_bounded_bilinear_map.fderiv {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) :
fderiv 𝕜 b p = h.deriv p
theorem is_bounded_bilinear_map.fderiv_within {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} {u : set (E × F)} (h : is_bounded_bilinear_map 𝕜 b) (p : E × F) (hxs : unique_diff_within_at 𝕜 u p) :
fderiv_within 𝕜 b u p = h.deriv p
theorem is_bounded_bilinear_map.differentiable_on {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {b : E × F G} {u : set (E × F)} (h : is_bounded_bilinear_map 𝕜 b) :
theorem continuous_linear_map.has_fderiv_within_at_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {G' : Type u_5} [normed_add_comm_group G'] [normed_space 𝕜 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 : has_fderiv_within_at f f' s x) (hg : has_fderiv_within_at g g' s x) :
has_fderiv_within_at (λ (y : G'), (B (f y)) (g y)) (((continuous_linear_map.precompR G' B) (f x)) g' + ((continuous_linear_map.precompL G' B) f') (g x)) s x
theorem continuous_linear_map.has_fderiv_at_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {G' : Type u_5} [normed_add_comm_group G'] [normed_space 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' E} {g : G' F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F} {x : G'} (hf : has_fderiv_at f f' x) (hg : has_fderiv_at g g' x) :
has_fderiv_at (λ (y : G'), (B (f y)) (g y)) (((continuous_linear_map.precompR G' B) (f x)) g' + ((continuous_linear_map.precompL G' B) f') (g x)) x
theorem continuous_linear_map.fderiv_within_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {G' : Type u_5} [normed_add_comm_group G'] [normed_space 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' E} {g : G' F} {x : G'} {s : set G'} (hf : differentiable_within_at 𝕜 f s x) (hg : differentiable_within_at 𝕜 g s x) (hs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (λ (y : G'), (B (f y)) (g y)) s x = ((continuous_linear_map.precompR G' B) (f x)) (fderiv_within 𝕜 g s x) + ((continuous_linear_map.precompL G' B) (fderiv_within 𝕜 f s x)) (g x)
theorem continuous_linear_map.fderiv_of_bilinear {𝕜 : Type u_1} [nontrivially_normed_field 𝕜] {E : Type u_2} [normed_add_comm_group E] [normed_space 𝕜 E] {F : Type u_3} [normed_add_comm_group F] [normed_space 𝕜 F] {G : Type u_4} [normed_add_comm_group G] [normed_space 𝕜 G] {G' : Type u_5} [normed_add_comm_group G'] [normed_space 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' E} {g : G' F} {x : G'} (hf : differentiable_at 𝕜 f x) (hg : differentiable_at 𝕜 g x) :
fderiv 𝕜 (λ (y : G'), (B (f y)) (g y)) x = ((continuous_linear_map.precompR G' B) (f x)) (fderiv 𝕜 g x) + ((continuous_linear_map.precompL G' B) (fderiv 𝕜 f x)) (g x)