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}
[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]
{x : E}
(iso : E ≃L[𝕜] F) :
has_strict_fderiv_at ⇑iso ↑iso x
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
{s : set E}
(iso : E ≃L[𝕜] F) :
has_fderiv_within_at ⇑iso ↑iso s x
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
(iso : E ≃L[𝕜] F) :
has_fderiv_at ⇑iso ↑iso x
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
(iso : E ≃L[𝕜] F) :
differentiable_at 𝕜 ⇑iso x
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
{s : set E}
(iso : E ≃L[𝕜] F) :
differentiable_within_at 𝕜 ⇑iso s x
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
(iso : E ≃L[𝕜] F) :
@[protected]
theorem
continuous_linear_equiv.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]
{x : E}
{s : set E}
(iso : E ≃L[𝕜] F)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 ⇑iso s x = ↑iso
@[protected]
theorem
continuous_linear_equiv.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]
(iso : E ≃L[𝕜] F) :
differentiable 𝕜 ⇑iso
@[protected]
theorem
continuous_linear_equiv.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]
{s : set E}
(iso : E ≃L[𝕜] F) :
differentiable_on 𝕜 ⇑iso s
theorem
continuous_linear_equiv.comp_differentiable_within_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{s : set G}
{x : G} :
differentiable_within_at 𝕜 (⇑iso ∘ f) s x ↔ differentiable_within_at 𝕜 f s x
theorem
continuous_linear_equiv.comp_differentiable_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{x : G} :
differentiable_at 𝕜 (⇑iso ∘ f) x ↔ differentiable_at 𝕜 f x
theorem
continuous_linear_equiv.comp_differentiable_on_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{s : set G} :
differentiable_on 𝕜 (⇑iso ∘ f) s ↔ differentiable_on 𝕜 f s
theorem
continuous_linear_equiv.comp_differentiable_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E} :
differentiable 𝕜 (⇑iso ∘ f) ↔ differentiable 𝕜 f
theorem
continuous_linear_equiv.comp_has_fderiv_within_at_iff
{𝕜 : 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]
(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 ↔ has_fderiv_within_at f f' s x
theorem
continuous_linear_equiv.comp_has_strict_fderiv_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] E} :
has_strict_fderiv_at (⇑iso ∘ f) (↑iso.comp f') x ↔ has_strict_fderiv_at f f' x
theorem
continuous_linear_equiv.comp_has_fderiv_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] E} :
has_fderiv_at (⇑iso ∘ f) (↑iso.comp f') x ↔ has_fderiv_at f f' x
theorem
continuous_linear_equiv.comp_has_fderiv_within_at_iff'
{𝕜 : 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]
(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 ↔ has_fderiv_within_at f (↑(iso.symm).comp f') s x
theorem
continuous_linear_equiv.comp_has_fderiv_at_iff'
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] F} :
has_fderiv_at (⇑iso ∘ f) f' x ↔ has_fderiv_at f (↑(iso.symm).comp f') x
theorem
continuous_linear_equiv.comp_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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{s : set G}
{x : G}
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (⇑iso ∘ f) s x = ↑iso.comp (fderiv_within 𝕜 f s x)
theorem
continuous_linear_equiv.comp_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]
(iso : E ≃L[𝕜] F)
{f : G → E}
{x : G} :
theorem
continuous_linear_equiv.comp_right_differentiable_within_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{s : set F}
{x : E} :
differentiable_within_at 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ differentiable_within_at 𝕜 f s (⇑iso x)
theorem
continuous_linear_equiv.comp_right_differentiable_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{x : E} :
differentiable_at 𝕜 (f ∘ ⇑iso) x ↔ differentiable_at 𝕜 f (⇑iso x)
theorem
continuous_linear_equiv.comp_right_differentiable_on_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{s : set F} :
differentiable_on 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ differentiable_on 𝕜 f s
theorem
continuous_linear_equiv.comp_right_differentiable_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G} :
differentiable 𝕜 (f ∘ ⇑iso) ↔ differentiable 𝕜 f
theorem
continuous_linear_equiv.comp_right_has_fderiv_within_at_iff
{𝕜 : 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]
(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 ↔ has_fderiv_within_at f f' s (⇑iso x)
theorem
continuous_linear_equiv.comp_right_has_fderiv_at_iff
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{x : E}
{f' : F →L[𝕜] G} :
has_fderiv_at (f ∘ ⇑iso) (f'.comp ↑iso) x ↔ has_fderiv_at f f' (⇑iso x)
theorem
continuous_linear_equiv.comp_right_has_fderiv_within_at_iff'
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{s : set F}
{x : E}
{f' : E →L[𝕜] G} :
theorem
continuous_linear_equiv.comp_right_has_fderiv_at_iff'
{𝕜 : 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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{x : E}
{f' : E →L[𝕜] G} :
has_fderiv_at (f ∘ ⇑iso) f' x ↔ has_fderiv_at f (f'.comp ↑(iso.symm)) (⇑iso x)
theorem
continuous_linear_equiv.comp_right_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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{s : set F}
{x : E}
(hxs : unique_diff_within_at 𝕜 (⇑iso ⁻¹' s) x) :
fderiv_within 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = (fderiv_within 𝕜 f s (⇑iso x)).comp ↑iso
theorem
continuous_linear_equiv.comp_right_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]
(iso : E ≃L[𝕜] F)
{f : F → G}
{x : E} :
Differentiability of linear isometry equivs, and invariance of differentiability #
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
(iso : E ≃ₗᵢ[𝕜] F) :
has_strict_fderiv_at ⇑iso ↑iso x
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
{s : set E}
(iso : E ≃ₗᵢ[𝕜] F) :
has_fderiv_within_at ⇑iso ↑iso s x
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
(iso : E ≃ₗᵢ[𝕜] F) :
has_fderiv_at ⇑iso ↑iso x
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
(iso : E ≃ₗᵢ[𝕜] F) :
differentiable_at 𝕜 ⇑iso x
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
{s : set E}
(iso : E ≃ₗᵢ[𝕜] F) :
differentiable_within_at 𝕜 ⇑iso s x
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
(iso : E ≃ₗᵢ[𝕜] F) :
@[protected]
theorem
linear_isometry_equiv.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]
{x : E}
{s : set E}
(iso : E ≃ₗᵢ[𝕜] F)
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 ⇑iso s x = ↑iso
@[protected]
theorem
linear_isometry_equiv.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]
(iso : E ≃ₗᵢ[𝕜] F) :
differentiable 𝕜 ⇑iso
@[protected]
theorem
linear_isometry_equiv.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]
{s : set E}
(iso : E ≃ₗᵢ[𝕜] F) :
differentiable_on 𝕜 ⇑iso s
theorem
linear_isometry_equiv.comp_differentiable_within_at_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{s : set G}
{x : G} :
differentiable_within_at 𝕜 (⇑iso ∘ f) s x ↔ differentiable_within_at 𝕜 f s x
theorem
linear_isometry_equiv.comp_differentiable_at_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{x : G} :
differentiable_at 𝕜 (⇑iso ∘ f) x ↔ differentiable_at 𝕜 f x
theorem
linear_isometry_equiv.comp_differentiable_on_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{s : set G} :
differentiable_on 𝕜 (⇑iso ∘ f) s ↔ differentiable_on 𝕜 f s
theorem
linear_isometry_equiv.comp_differentiable_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E} :
differentiable 𝕜 (⇑iso ∘ f) ↔ differentiable 𝕜 f
theorem
linear_isometry_equiv.comp_has_fderiv_within_at_iff
{𝕜 : 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]
(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 ↔ has_fderiv_within_at f f' s x
theorem
linear_isometry_equiv.comp_has_strict_fderiv_at_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] E} :
has_strict_fderiv_at (⇑iso ∘ f) (↑iso.comp f') x ↔ has_strict_fderiv_at f f' x
theorem
linear_isometry_equiv.comp_has_fderiv_at_iff
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] E} :
has_fderiv_at (⇑iso ∘ f) (↑iso.comp f') x ↔ has_fderiv_at f f' x
theorem
linear_isometry_equiv.comp_has_fderiv_within_at_iff'
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{s : set G}
{x : G}
{f' : G →L[𝕜] F} :
has_fderiv_within_at (⇑iso ∘ f) f' s x ↔ has_fderiv_within_at f (↑(iso.symm).comp f') s x
theorem
linear_isometry_equiv.comp_has_fderiv_at_iff'
{𝕜 : 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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{x : G}
{f' : G →L[𝕜] F} :
has_fderiv_at (⇑iso ∘ f) f' x ↔ has_fderiv_at f (↑(iso.symm).comp f') x
theorem
linear_isometry_equiv.comp_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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{s : set G}
{x : G}
(hxs : unique_diff_within_at 𝕜 s x) :
fderiv_within 𝕜 (⇑iso ∘ f) s x = ↑iso.comp (fderiv_within 𝕜 f s x)
theorem
linear_isometry_equiv.comp_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]
(iso : E ≃ₗᵢ[𝕜] F)
{f : G → E}
{x : G} :
theorem
has_strict_fderiv_at.of_local_left_inverse
{𝕜 : 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}
{f' : E ≃L[𝕜] F}
{g : F → E}
{a : F}
(hg : continuous_at g a)
(hf : has_strict_fderiv_at f ↑f' (g a))
(hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
has_strict_fderiv_at g ↑(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}
[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}
{f' : E ≃L[𝕜] F}
{g : F → E}
{a : F}
(hg : continuous_at g a)
(hf : has_fderiv_at f ↑f' (g a))
(hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :
has_fderiv_at g ↑(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}
[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 : local_homeomorph E F)
{f' : E ≃L[𝕜] F}
{a : F}
(ha : a ∈ f.to_local_equiv.target)
(htff' : has_strict_fderiv_at ⇑f ↑f' (⇑(f.symm) a)) :
has_strict_fderiv_at ⇑(f.symm) ↑(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}
[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 : local_homeomorph E F)
{f' : E ≃L[𝕜] F}
{a : F}
(ha : a ∈ f.to_local_equiv.target)
(htff' : has_fderiv_at ⇑f ↑f' (⇑(f.symm) a)) :
has_fderiv_at ⇑(f.symm) ↑(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}
[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}
{f' : E →L[𝕜] F}
{x : E}
{s : set E}
(h : has_fderiv_within_at f f' s x)
(hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖⇑f' z‖) :
theorem
has_fderiv_at.eventually_ne
{𝕜 : 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}
{f' : E →L[𝕜] F}
{x : E}
(h : has_fderiv_at f f' x)
(hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖⇑f' z‖) :
theorem
has_fderiv_at_filter_real_equiv
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
{f : E → F}
{f' : E →L[ℝ] F}
{x : E}
{L : filter E} :
theorem
has_fderiv_at.lim_real
{E : Type u_1}
[normed_add_comm_group E]
[normed_space ℝ E]
{F : Type u_2}
[normed_add_comm_group F]
[normed_space ℝ F]
{f : E → F}
{f' : E →L[ℝ] F}
{x : E}
(hf : has_fderiv_at f 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}
[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}
{f' : E →L[𝕜] F}
{x : E}
(h : has_fderiv_within_at f f' s x) :
set.maps_to ⇑f' (tangent_cone_at 𝕜 s x) (tangent_cone_at 𝕜 (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}
[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}
{f' : E →L[𝕜] F}
{x : E}
(h : has_fderiv_within_at f f' s x)
(hs : unique_diff_within_at 𝕜 s x)
(h' : dense_range ⇑f') :
unique_diff_within_at 𝕜 (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}
[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}
{f' : E → (E →L[𝕜] F)}
(hs : unique_diff_on 𝕜 s)
(hf' : ∀ (x : E), x ∈ s → has_fderiv_within_at f (f' x) s x)
(hd : ∀ (x : E), x ∈ s → dense_range ⇑(f' x)) :
unique_diff_on 𝕜 (f '' s)
theorem
has_fderiv_within_at.unique_diff_within_at_of_continuous_linear_equiv
{𝕜 : 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}
{x : E}
(e' : E ≃L[𝕜] F)
(h : has_fderiv_within_at f ↑e' s x)
(hs : unique_diff_within_at 𝕜 s x) :
unique_diff_within_at 𝕜 (f '' s) (f x)
theorem
continuous_linear_equiv.unique_diff_on_image
{𝕜 : 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]
{s : set E}
(e : E ≃L[𝕜] F)
(h : unique_diff_on 𝕜 s) :
unique_diff_on 𝕜 (⇑e '' s)
@[simp]
theorem
continuous_linear_equiv.unique_diff_on_image_iff
{𝕜 : 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]
{s : set E}
(e : E ≃L[𝕜] F) :
unique_diff_on 𝕜 (⇑e '' s) ↔ unique_diff_on 𝕜 s
@[simp]
theorem
continuous_linear_equiv.unique_diff_on_preimage_iff
{𝕜 : 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]
{s : set E}
(e : F ≃L[𝕜] E) :
unique_diff_on 𝕜 (⇑e ⁻¹' s) ↔ unique_diff_on 𝕜 s