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.

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) (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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) (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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) (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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 = ↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)

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 = ↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)

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 (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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 (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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 (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) 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 (↑(ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm iso).toLinearEquiv)) 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 (↑(ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm iso).toLinearEquiv)) 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 (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) (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 (↑(ContinuousLinearEquiv.mk iso.toLinearEquiv)) (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 LocalHomeomorph.hasStrictFDerivAt_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : LocalHomeomorph E F) {f' : E ≃L[𝕜] F} {a : F} (ha : a ∈ f.target) (htff' : HasStrictFDerivAt (↑f) (↑f') (↑(LocalHomeomorph.symm f) a)) :

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

source

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

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

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' => ‖x' - x‖⁻¹ * ‖f x' - f x - ↑f' (x' - x)‖) L (nhds 0) ↔ Filter.Tendsto (fun x' => ‖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 : E), x ∈ s → HasFDerivWithinAt f (f' x) s x) (hd : ∀ (x : E), 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