# mathlib3documentation

analysis.calculus.fderiv.equiv

# The derivative of a linear equivalence #

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 continuous linear equivalences.

### Differentiability of linear equivs, and invariance of differentiability #

@[protected]
theorem continuous_linear_equiv.has_strict_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃L[𝕜] F) :
iso x
@[protected]
theorem continuous_linear_equiv.has_fderiv_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃L[𝕜] F) :
iso s x
@[protected]
theorem continuous_linear_equiv.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃L[𝕜] F) :
iso x
@[protected]
theorem continuous_linear_equiv.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃L[𝕜] F) :
iso x
@[protected]
theorem continuous_linear_equiv.differentiable_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃L[𝕜] F) :
s x
@[protected]
theorem continuous_linear_equiv.fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃L[𝕜] F) :
iso x = iso
@[protected]
theorem continuous_linear_equiv.fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃L[𝕜] F) (hxs : x) :
iso s x = iso
@[protected]
theorem continuous_linear_equiv.differentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (iso : E ≃L[𝕜] F) :
iso
@[protected]
theorem continuous_linear_equiv.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (iso : E ≃L[𝕜] F) :
iso s
theorem continuous_linear_equiv.comp_differentiable_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {s : set G} {x : G} :
(iso f) s x x
theorem continuous_linear_equiv.comp_differentiable_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {x : G} :
(iso f) x x
theorem continuous_linear_equiv.comp_differentiable_on_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {s : set G} :
(iso f) s s
theorem continuous_linear_equiv.comp_differentiable_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} :
(iso f)
theorem continuous_linear_equiv.comp_has_fderiv_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {s : set G} {x : G} {f' : G →L[𝕜] E} :
has_fderiv_within_at (iso f) (iso.comp f') s x s x
theorem continuous_linear_equiv.comp_has_strict_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] E} :
has_strict_fderiv_at (iso f) (iso.comp f') x x
theorem continuous_linear_equiv.comp_has_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] E} :
has_fderiv_at (iso f) (iso.comp f') x f' x
theorem continuous_linear_equiv.comp_has_fderiv_within_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {s : set G} {x : G} {f' : G →L[𝕜] F} :
has_fderiv_within_at (iso f) f' s x ((iso.symm).comp f') s x
theorem continuous_linear_equiv.comp_has_fderiv_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] F} :
has_fderiv_at (iso f) f' x ((iso.symm).comp f') x
theorem continuous_linear_equiv.comp_fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {s : set G} {x : G} (hxs : x) :
(iso f) s x = iso.comp f s x)
theorem continuous_linear_equiv.comp_fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : G E} {x : G} :
(iso f) x = iso.comp (fderiv 𝕜 f x)
theorem continuous_linear_equiv.comp_right_differentiable_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {s : set F} {x : E} :
(f iso) (iso ⁻¹' s) x (iso x)
theorem continuous_linear_equiv.comp_right_differentiable_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {x : E} :
(f iso) x (iso x)
theorem continuous_linear_equiv.comp_right_differentiable_on_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {s : set F} :
(f iso) (iso ⁻¹' s) s
theorem continuous_linear_equiv.comp_right_differentiable_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} :
(f iso)
theorem continuous_linear_equiv.comp_right_has_fderiv_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {s : set F} {x : E} {f' : F →L[𝕜] G} :
has_fderiv_within_at (f iso) (f'.comp iso) (iso ⁻¹' s) x s (iso x)
theorem continuous_linear_equiv.comp_right_has_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {x : E} {f' : F →L[𝕜] G} :
has_fderiv_at (f iso) (f'.comp iso) x f' (iso x)
theorem continuous_linear_equiv.comp_right_has_fderiv_within_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {s : set F} {x : E} {f' : E →L[𝕜] G} :
has_fderiv_within_at (f iso) f' (iso ⁻¹' s) x (f'.comp (iso.symm)) s (iso x)
theorem continuous_linear_equiv.comp_right_has_fderiv_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {x : E} {f' : E →L[𝕜] G} :
has_fderiv_at (f iso) f' x (f'.comp (iso.symm)) (iso x)
theorem continuous_linear_equiv.comp_right_fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {s : set F} {x : E} (hxs : (iso ⁻¹' s) x) :
(f iso) (iso ⁻¹' s) x = f s (iso x)).comp iso
theorem continuous_linear_equiv.comp_right_fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃L[𝕜] F) {f : F G} {x : E} :
(f iso) x = (fderiv 𝕜 f (iso x)).comp iso

### Differentiability of linear isometry equivs, and invariance of differentiability #

@[protected]
theorem linear_isometry_equiv.has_strict_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
iso x
@[protected]
theorem linear_isometry_equiv.has_fderiv_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃ₗᵢ[𝕜] F) :
iso s x
@[protected]
theorem linear_isometry_equiv.has_fderiv_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
iso x
@[protected]
theorem linear_isometry_equiv.differentiable_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
iso x
@[protected]
theorem linear_isometry_equiv.differentiable_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃ₗᵢ[𝕜] F) :
s x
@[protected]
theorem linear_isometry_equiv.fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :
iso x = iso
@[protected]
theorem linear_isometry_equiv.fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {x : E} {s : set E} (iso : E ≃ₗᵢ[𝕜] F) (hxs : x) :
iso s x = iso
@[protected]
theorem linear_isometry_equiv.differentiable {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (iso : E ≃ₗᵢ[𝕜] F) :
iso
@[protected]
theorem linear_isometry_equiv.differentiable_on {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (iso : E ≃ₗᵢ[𝕜] F) :
iso s
theorem linear_isometry_equiv.comp_differentiable_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {s : set G} {x : G} :
(iso f) s x x
theorem linear_isometry_equiv.comp_differentiable_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {x : G} :
(iso f) x x
theorem linear_isometry_equiv.comp_differentiable_on_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {s : set G} :
(iso f) s s
theorem linear_isometry_equiv.comp_differentiable_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} :
(iso f)
theorem linear_isometry_equiv.comp_has_fderiv_within_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {s : set G} {x : G} {f' : G →L[𝕜] E} :
has_fderiv_within_at (iso f) (iso.comp f') s x s x
theorem linear_isometry_equiv.comp_has_strict_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] E} :
has_strict_fderiv_at (iso f) (iso.comp f') x x
theorem linear_isometry_equiv.comp_has_fderiv_at_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] E} :
has_fderiv_at (iso f) (iso.comp f') x f' x
theorem linear_isometry_equiv.comp_has_fderiv_within_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {s : set G} {x : G} {f' : G →L[𝕜] F} :
has_fderiv_within_at (iso f) f' s x ((iso.symm).comp f') s x
theorem linear_isometry_equiv.comp_has_fderiv_at_iff' {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {x : G} {f' : G →L[𝕜] F} :
has_fderiv_at (iso f) f' x ((iso.symm).comp f') x
theorem linear_isometry_equiv.comp_fderiv_within {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {s : set G} {x : G} (hxs : x) :
(iso f) s x = iso.comp f s x)
theorem linear_isometry_equiv.comp_fderiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {G : Type u_4} [ G] (iso : E ≃ₗᵢ[𝕜] F) {f : G E} {x : G} :
(iso f) x = iso.comp (fderiv 𝕜 f x)
theorem has_strict_fderiv_at.of_local_left_inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E ≃L[𝕜] F} {g : F E} {a : F} (hg : a) (hf : (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
(f'.symm) a

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a in the strict sense, then g has the derivative f'⁻¹ at a in the strict sense.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem has_fderiv_at.of_local_left_inverse {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E ≃L[𝕜] F} {g : F E} {a : F} (hg : a) (hf : f' (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
(f'.symm) a

If f (g y) = y for y in some neighborhood of a, g is continuous at a, and f has an invertible derivative f' at g a, then g has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem local_homeomorph.has_strict_fderiv_at_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : F) {f' : E ≃L[𝕜] F} {a : F} (ha : a f.to_local_equiv.target) (htff' : ((f.symm) a)) :
(f'.symm) a

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has an invertible derivative f' in the sense of strict differentiability at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem local_homeomorph.has_fderiv_at_symm {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] (f : F) {f' : E ≃L[𝕜] F} {a : F} (ha : a f.to_local_equiv.target) (htff' : f' ((f.symm) a)) :
(f'.symm) a

If f is a local homeomorphism defined on a neighbourhood of f.symm a, and f has an invertible derivative f' at f.symm a, then f.symm has the derivative f'⁻¹ at a.

This is one of the easy parts of the inverse function theorem: it assumes that we already have an inverse function.

theorem has_fderiv_within_at.eventually_ne {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} {s : set E} (h : s x) (hf' : (C : ), (z : E), z C * f' z) :
∀ᶠ (z : E) in (s \ {x}), f z f x
theorem has_fderiv_at.eventually_ne {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {f' : E →L[𝕜] F} {x : E} (h : f' x) (hf' : (C : ), (z : E), z C * f' z) :
∀ᶠ (z : E) in {x}, f z f x
theorem has_fderiv_at_filter_real_equiv {E : Type u_1} [ E] {F : Type u_2} [ F] {f : E F} {f' : E →L[] F} {x : E} {L : filter E} :
filter.tendsto (λ (x' : E), x' - x⁻¹ * f x' - f x - f' (x' - x)) L (nhds 0) filter.tendsto (λ (x' : E), x' - x⁻¹ (f x' - f x - f' (x' - x))) L (nhds 0)
theorem has_fderiv_at.lim_real {E : Type u_1} [ E] {F : Type u_2} [ F] {f : E F} {f' : E →L[] F} {x : E} (hf : f' x) (v : E) :
filter.tendsto (λ (c : ), c (f (x + c⁻¹ v) - f x)) filter.at_top (nhds (f' v))
theorem has_fderiv_within_at.maps_to_tangent_cone {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {f' : E →L[𝕜] F} {x : E} (h : s x) :
s x) (f '' s) (f x))

The image of a tangent cone under the differential of a map is included in the tangent cone to the image.

theorem has_fderiv_within_at.unique_diff_within_at {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {f' : E →L[𝕜] F} {x : E} (h : s x) (hs : x) (h' : dense_range f') :
(f '' s) (f x)

If a set has the unique differentiability property at a point x, then the image of this set under a map with onto derivative has also the unique differentiability property at the image point.

theorem unique_diff_on.image {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {f' : E (E →L[𝕜] F)} (hs : s) (hf' : (x : E), x s (f' x) s x) (hd : (x : E), x s dense_range (f' x)) :
(f '' s)
theorem has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {f : E F} {s : set E} {x : E} (e' : E ≃L[𝕜] F) (h : s x) (hs : x) :
(f '' s) (f x)
theorem continuous_linear_equiv.unique_diff_on_image {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (e : E ≃L[𝕜] F) (h : s) :
(e '' s)
@[simp]
theorem continuous_linear_equiv.unique_diff_on_image_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (e : E ≃L[𝕜] F) :
(e '' s)
@[simp]
theorem continuous_linear_equiv.unique_diff_on_preimage_iff {𝕜 : Type u_1} {E : Type u_2} [ E] {F : Type u_3} [ F] {s : set E} (e : F ≃L[𝕜] E) :
(e ⁻¹' s)