mathlib3 documentation

analysis.calculus.fderiv.linear

The derivative of bounded linear 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 linear maps.

Continuous linear maps #

There are currently two variants of these in mathlib, the bundled version (named continuous_linear_map, and denoted E →L[𝕜] F), and the unbundled version (with a predicate is_bounded_linear_map). We give statements for both versions.

@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} :
@[protected]
theorem continuous_linear_map.has_fderiv_at_filter {𝕜 : 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] (e : E →L[𝕜] F) {x : E} {L : filter E} :
@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} {s : set E} :
@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} :
@[protected, simp]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} :
@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} {s : set E} :
@[protected, simp]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} :
fderiv 𝕜 e x = e
@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {x : E} {s : set E} (hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 e s x = e
@[protected, simp]
theorem continuous_linear_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] (e : E →L[𝕜] F) :
@[protected]
theorem continuous_linear_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] (e : E →L[𝕜] F) {s : set E} :
theorem is_bounded_linear_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] {f : E F} {x : E} (h : is_bounded_linear_map 𝕜 f) :
theorem is_bounded_linear_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] {f : E F} {x : E} {s : set E} (h : is_bounded_linear_map 𝕜 f) :
theorem is_bounded_linear_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] {f : E F} {x : E} (h : is_bounded_linear_map 𝕜 f) :
theorem is_bounded_linear_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] {f : E F} {x : E} {s : set E} (h : is_bounded_linear_map 𝕜 f) (hxs : unique_diff_within_at 𝕜 s x) :
theorem is_bounded_linear_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] {f : E F} {s : set E} (h : is_bounded_linear_map 𝕜 f) :