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) :
has_strict_fderiv_at b (h.deriv p) p
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) :
has_fderiv_at b (h.deriv p) p
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) :
has_fderiv_within_at b (h.deriv p) u p
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) :
differentiable_at 𝕜 b p
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) :
differentiable_within_at 𝕜 b u p
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) :
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
{𝕜 : 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) :
differentiable 𝕜 b
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) :
differentiable_on 𝕜 b u
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) :