The derivative of a linear equivalence #

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.

We also prove the usual formula for the derivative of the inverse function, assuming it exists. The inverse function theorem is in Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean.

Differentiability of linear equivs, and invariance of differentiability #

source

theorem ContinuousLinearEquiv.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :

HasStrictFDerivAt (⇑iso) (↑iso) x

source

theorem ContinuousLinearEquiv.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) :

HasFDerivWithinAt (⇑iso) (↑iso) s x

source

theorem ContinuousLinearEquiv.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :

HasFDerivAt (⇑iso) (↑iso) x

source

theorem ContinuousLinearEquiv.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :

DifferentiableAt 𝕜 (⇑iso) x

source

theorem ContinuousLinearEquiv.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) :

DifferentiableWithinAt 𝕜 (⇑iso) s x

source

theorem ContinuousLinearEquiv.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃L[𝕜] F) :

fderiv 𝕜 (⇑iso) x = ↑iso

source

theorem ContinuousLinearEquiv.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃L[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (⇑iso) s x = ↑iso

source

theorem ContinuousLinearEquiv.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (iso : E ≃L[𝕜] F) :

Differentiable 𝕜 ⇑iso

source

theorem ContinuousLinearEquiv.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (iso : E ≃L[𝕜] F) :

DifferentiableOn 𝕜 (⇑iso) s

source

theorem ContinuousLinearEquiv.comp_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} :

DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

source

theorem ContinuousLinearEquiv.comp_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} :

DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

source

theorem ContinuousLinearEquiv.comp_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} :

DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s

source

theorem ContinuousLinearEquiv.comp_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} :

Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f

source

theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :

HasFDerivWithinAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑iso) f') s x ↔ HasFDerivWithinAt f f' s x

source

theorem ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :

HasStrictFDerivAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑iso) f') x ↔ HasStrictFDerivAt f f' x

source

theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :

HasFDerivAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑iso) f') x ↔ HasFDerivAt f f' x

source

theorem ContinuousLinearEquiv.comp_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :

HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm iso)) f') s x

source

theorem ContinuousLinearEquiv.comp_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F} :

HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f (ContinuousLinearMap.comp (↑(ContinuousLinearEquiv.symm iso)) f') x

source

theorem ContinuousLinearEquiv.comp_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (⇑iso ∘ f) s x = ContinuousLinearMap.comp (↑iso) (fderivWithin 𝕜 f s x)

source

theorem ContinuousLinearEquiv.comp_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} :

fderiv 𝕜 (⇑iso ∘ f) x = ContinuousLinearMap.comp (↑iso) (fderiv 𝕜 f x)

source

theorem ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} :

DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)

source

theorem ContinuousLinearEquiv.comp_right_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} :

DifferentiableAt 𝕜 (f ∘ ⇑iso) x ↔ DifferentiableAt 𝕜 f (iso x)

source

theorem ContinuousLinearEquiv.comp_right_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} :

DifferentiableOn 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) ↔ DifferentiableOn 𝕜 f s

source

theorem ContinuousLinearEquiv.comp_right_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} :

Differentiable 𝕜 (f ∘ ⇑iso) ↔ Differentiable 𝕜 f

source

theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} {f' : F →L[𝕜] G} :

HasFDerivWithinAt (f ∘ ⇑iso) (ContinuousLinearMap.comp f' ↑iso) (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f f' s (iso x)

source

theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : F →L[𝕜] G} :

HasFDerivAt (f ∘ ⇑iso) (ContinuousLinearMap.comp f' ↑iso) x ↔ HasFDerivAt f f' (iso x)

source

theorem ContinuousLinearEquiv.comp_right_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} {f' : E →L[𝕜] G} :

HasFDerivWithinAt (f ∘ ⇑iso) f' (⇑iso ⁻¹' s) x ↔ HasFDerivWithinAt f (ContinuousLinearMap.comp f' ↑(ContinuousLinearEquiv.symm iso)) s (iso x)

source

theorem ContinuousLinearEquiv.comp_right_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} {f' : E →L[𝕜] G} :

HasFDerivAt (f ∘ ⇑iso) f' x ↔ HasFDerivAt f (ContinuousLinearMap.comp f' ↑(ContinuousLinearEquiv.symm iso)) (iso x)

source

theorem ContinuousLinearEquiv.comp_right_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E} (hxs : UniqueDiffWithinAt 𝕜 (⇑iso ⁻¹' s) x) :

fderivWithin 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x = ContinuousLinearMap.comp (fderivWithin 𝕜 f s (iso x)) ↑iso

source

theorem ContinuousLinearEquiv.comp_right_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {x : E} :

fderiv 𝕜 (f ∘ ⇑iso) x = ContinuousLinearMap.comp (fderiv 𝕜 f (iso x)) ↑iso

Differentiability of linear isometry equivs, and invariance of differentiability #

source

theorem LinearIsometryEquiv.hasStrictFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :

HasStrictFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x

source

theorem LinearIsometryEquiv.hasFDerivWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :

HasFDerivWithinAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) s x

source

theorem LinearIsometryEquiv.hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :

HasFDerivAt (⇑iso) (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) x

source

theorem LinearIsometryEquiv.differentiableAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :

DifferentiableAt 𝕜 (⇑iso) x

source

theorem LinearIsometryEquiv.differentiableWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :

DifferentiableWithinAt 𝕜 (⇑iso) s x

source

theorem LinearIsometryEquiv.fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (iso : E ≃ₗᵢ[𝕜] F) :

fderiv 𝕜 (⇑iso) x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

source

theorem LinearIsometryEquiv.fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (⇑iso) s x = ↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

source

theorem LinearIsometryEquiv.differentiable {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (iso : E ≃ₗᵢ[𝕜] F) :

Differentiable 𝕜 ⇑iso

source

theorem LinearIsometryEquiv.differentiableOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (iso : E ≃ₗᵢ[𝕜] F) :

DifferentiableOn 𝕜 (⇑iso) s

source

theorem LinearIsometryEquiv.comp_differentiableWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} :

DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x ↔ DifferentiableWithinAt 𝕜 f s x

source

theorem LinearIsometryEquiv.comp_differentiableAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} :

DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x

source

theorem LinearIsometryEquiv.comp_differentiableOn_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} :

DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s

source

theorem LinearIsometryEquiv.comp_differentiable_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} :

Differentiable 𝕜 (⇑iso ∘ f) ↔ Differentiable 𝕜 f

source

theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] E} :

HasFDerivWithinAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) f') s x ↔ HasFDerivWithinAt f f' s x

source

theorem LinearIsometryEquiv.comp_hasStrictFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :

HasStrictFDerivAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) f') x ↔ HasStrictFDerivAt f f' x

source

theorem LinearIsometryEquiv.comp_hasFDerivAt_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E} :

HasFDerivAt (⇑iso ∘ f) (ContinuousLinearMap.comp (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) f') x ↔ HasFDerivAt f f' x

source

theorem LinearIsometryEquiv.comp_hasFDerivWithinAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :

HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.comp (↑{ toLinearEquiv := (LinearIsometryEquiv.symm iso).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) f') s x

source

theorem LinearIsometryEquiv.comp_hasFDerivAt_iff' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] F} :

HasFDerivAt (⇑iso ∘ f) f' x ↔ HasFDerivAt f (ContinuousLinearMap.comp (↑{ toLinearEquiv := (LinearIsometryEquiv.symm iso).toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) f') x

source

theorem LinearIsometryEquiv.comp_fderivWithin {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {s : Set G} {x : G} (hxs : UniqueDiffWithinAt 𝕜 s x) :

fderivWithin 𝕜 (⇑iso ∘ f) s x = ContinuousLinearMap.comp (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) (fderivWithin 𝕜 f s x)

source

theorem LinearIsometryEquiv.comp_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {G : Type u_4} [NormedAddCommGroup G] [NormedSpace 𝕜 G] (iso : E ≃ₗᵢ[𝕜] F) {f : G → E} {x : G} :

fderiv 𝕜 (⇑iso ∘ f) x = ContinuousLinearMap.comp (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }) (fderiv 𝕜 f x)

source

theorem HasStrictFDerivAt.of_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasStrictFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :

HasStrictFDerivAt g (↑(ContinuousLinearEquiv.symm f')) 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.

source

theorem HasFDerivAt.of_local_left_inverse {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E ≃L[𝕜] F} {g : F → E} {a : F} (hg : ContinuousAt g a) (hf : HasFDerivAt f (↑f') (g a)) (hfg : ∀ᶠ (y : F) in nhds a, f (g y) = y) :

HasFDerivAt g (↑(ContinuousLinearEquiv.symm f')) 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.

source

theorem PartialHomeomorph.hasStrictFDerivAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt (↑f) (↑f') (↑(PartialHomeomorph.symm f) a)) :

HasStrictFDerivAt (↑(PartialHomeomorph.symm f)) (↑(ContinuousLinearEquiv.symm f')) a

If f is a partial 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.

source

theorem PartialHomeomorph.hasFDerivAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : PartialHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasFDerivAt (↑f) (↑f') (↑(PartialHomeomorph.symm f) a)) :

HasFDerivAt (↑(PartialHomeomorph.symm f)) (↑(ContinuousLinearEquiv.symm f')) a

If f is a partial 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.

source

theorem HasFDerivWithinAt.eventually_ne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} (h : HasFDerivWithinAt f f' s x) (hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖) :

∀ᶠ (z : E) in nhdsWithin x (s \ {x}), f z ≠ f x

source

theorem HasFDerivAt.eventually_ne {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivAt f f' x) (hf' : ∃ (C : ℝ), ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖) :

∀ᶠ (z : E) in nhdsWithin x {x}ᶜ, f z ≠ f x

source

theorem has_fderiv_at_filter_real_equiv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ ] F} {x : E} {L : Filter E} :

Filter.Tendsto (fun (x' : E) => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (nhds 0) ↔ Filter.Tendsto (fun (x' : E) => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (nhds 0)

source

theorem HasFDerivAt.lim_real {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E → F} {f' : E →L[ℝ ] F} {x : E} (hf : HasFDerivAt f f' x) (v : E) :

Filter.Tendsto (fun (c : ℝ) => c • (f (x + c⁻¹ • v) - f x)) Filter.atTop (nhds (f' v))

source

theorem HasFDerivWithinAt.mapsTo_tangent_cone {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivWithinAt f f' s x) :

Set.MapsTo (⇑f') (tangentConeAt 𝕜 s x) (tangentConeAt 𝕜 (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.

source

theorem HasFDerivWithinAt.uniqueDiffWithinAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E →L[𝕜] F} {x : E} (h : HasFDerivWithinAt f f' s x) (hs : UniqueDiffWithinAt 𝕜 s x) (h' : DenseRange ⇑f') :

UniqueDiffWithinAt 𝕜 (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.

source

theorem UniqueDiffOn.image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {f' : E → E →L[𝕜] F} (hs : UniqueDiffOn 𝕜 s) (hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) (hd : ∀ x ∈ s, DenseRange ⇑(f' x)) :

UniqueDiffOn 𝕜 (f '' s)

source

theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (e' : E ≃L[𝕜] F) (h : HasFDerivWithinAt f (↑e') s x) (hs : UniqueDiffWithinAt 𝕜 s x) :

UniqueDiffWithinAt 𝕜 (f '' s) (f x)

source

theorem ContinuousLinearEquiv.uniqueDiffOn_image {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : E ≃L[𝕜] F) (h : UniqueDiffOn 𝕜 s) :

UniqueDiffOn 𝕜 (⇑e '' s)

source

@[simp]

theorem ContinuousLinearEquiv.uniqueDiffOn_image_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : E ≃L[𝕜] F) :

UniqueDiffOn 𝕜 (⇑e '' s) ↔ UniqueDiffOn 𝕜 s

source

@[simp]

theorem ContinuousLinearEquiv.uniqueDiffOn_preimage_iff {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : F ≃L[𝕜] E) :

UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Documentation

Mathlib.Analysis.Calculus.FDeriv.Equiv

The derivative of a linear equivalence #

Differentiability of linear equivs, and invariance of differentiability #

Differentiability of linear isometry equivs, and invariance of differentiability #