Derivatives under local and linear equivalences

Mathlib's OpenPartialHomeomorph.hasFDerivAt_symm computes the derivative of the inverse from an invertible derivative of the map. Without assuming that invertibility, this file records that when both the map and its inverse are differentiable at corresponding points, their derivatives compose to the identity. It does so for open partial homeomorphisms, and for a map Φ differentiable on an open set U and mapping it into an open set V, with an inverse Ψ differentiable on V (Φ ∘ Ψ = id on V and Ψ ∘ Φ = id on U).

Main results

• OpenPartialHomeomorph.fderiv_symm_comp_fderiv: the derivative of the inverse is a left inverse of the derivative.
• OpenPartialHomeomorph.fderiv_comp_fderiv_symm: the derivative of the inverse is a right inverse of the derivative.
• OpenPartialHomeomorph.fderiv_symm_apply_fderiv_apply, OpenPartialHomeomorph.fderiv_apply_fderiv_symm_apply: the same identities evaluated at a vector.
• TauCeti.fderiv_comp_fderiv_eq_id_of_invOn: DΦ(y) ∘ DΨ(Φ y) = id.
• ContinuousLinearEquiv.image_vanishingFDeriv_comp: precomposition by a continuous linear equivalence preserves the image of the vanishing-derivative locus.

Precomposition by a continuous linear equivalence preserves the image of the vanishing-derivative locus, with no differentiability premise. This follows the totalized derivative calculation in KLS, commit 65810c73f9dd7945fc646ab484cb19d673f5291d, formalization/FunctionalInequalities/Analysis/Sard/Basic.lean.

A point where a map has an antilipschitz derivative, such as an invertible derivative between finite-dimensional spaces, is isolated in its fibre (HasFDerivAt.eventually_ne). Hence a compact fibre consisting of such points is finite (IsCompact.finite_of_hasFDerivAt); this is the finiteness of the preimage of a regular value under a proper map.

theorem OpenPartialHomeomorph.fderiv_symm_comp_fderiv {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {p : F} (hp : p ∈ e.target) (hd : DifferentiableAt 𝕜 (↑e) (↑e.symm p)) (hds : DifferentiableAt 𝕜 (↑e.symm) p) : fderiv 𝕜 (↑e.symm) p ∘SL fderiv 𝕜 (↑e) (↑e.symm p) = ContinuousLinearMap.id 𝕜 E

The derivative of the inverse of an open partial homeomorphism at a point of its target is a left inverse of the derivative at the corresponding point of its source.

theorem OpenPartialHomeomorph.fderiv_comp_fderiv_symm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {p : F} (hp : p ∈ e.target) (hd : DifferentiableAt 𝕜 (↑e) (↑e.symm p)) (hds : DifferentiableAt 𝕜 (↑e.symm) p) : fderiv 𝕜 (↑e) (↑e.symm p) ∘SL fderiv 𝕜 (↑e.symm) p = ContinuousLinearMap.id 𝕜 F

The derivative of the inverse of an open partial homeomorphism at a point of its target is a right inverse of the derivative at the corresponding point of its source.

theorem OpenPartialHomeomorph.fderiv_symm_apply_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {p : F} (hp : p ∈ e.target) (hd : DifferentiableAt 𝕜 (↑e) (↑e.symm p)) (hds : DifferentiableAt 𝕜 (↑e.symm) p) (v : E) : (fderiv 𝕜 (↑e.symm) p) ((fderiv 𝕜 (↑e) (↑e.symm p)) v) = v

Pointwise form of OpenPartialHomeomorph.fderiv_symm_comp_fderiv.

theorem OpenPartialHomeomorph.fderiv_apply_fderiv_symm_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : OpenPartialHomeomorph E F) {p : F} (hp : p ∈ e.target) (hd : DifferentiableAt 𝕜 (↑e) (↑e.symm p)) (hds : DifferentiableAt 𝕜 (↑e.symm) p) (w : F) : (fderiv 𝕜 (↑e) (↑e.symm p)) ((fderiv 𝕜 (↑e.symm) p) w) = w

Pointwise form of OpenPartialHomeomorph.fderiv_comp_fderiv_symm.

theorem TauCeti.fderiv_comp_fderiv_eq_id_of_invOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {U : TopologicalSpace.Opens E} {V : TopologicalSpace.Opens F} {Φ : E → F} {Ψ : F → E} (hΦ : DifferentiableOn 𝕜 Φ ↑U) (hmaps : Set.MapsTo Φ ↑U ↑V) (hΨ : DifferentiableOn 𝕜 Ψ ↑V) (hΦΨ : Set.RightInvOn Ψ Φ ↑V) (hΨΦ : Set.LeftInvOn Ψ Φ ↑U) {y : E} (hy : y ∈ ↑U) : fderiv 𝕜 Φ y ∘SL fderiv 𝕜 Ψ (Φ y) = ContinuousLinearMap.id 𝕜 F

The derivative of the inverse. If Φ is differentiable on U and maps it into V, and Ψ, differentiable on V, is inverse to Φ (Φ ∘ Ψ = id on V, Ψ ∘ Φ = id on U), then DΦ(y) ∘ DΨ(Φ y) = id at every y ∈ U.

theorem ContinuousLinearEquiv.image_vanishingFDeriv_comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] (e : E ≃L[𝕜] F) (u : F → G) : u '' {x : F | fderiv 𝕜 u x = 0} = u ∘ ⇑e '' {y : E | fderiv 𝕜 (u ∘ ⇑e) y = 0}

Precomposition by a continuous linear equivalence preserves the image of the locus where the totalized Fréchet derivative vanishes. No differentiability hypothesis is needed.

theorem IsCompact.finite_of_hasFDerivAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E → E →L[𝕜] F} {y : F} (hK : IsCompact (f ⁻¹' {y})) (hf : ∀ x ∈ f ⁻¹' {y}, HasFDerivAt f (f' x) x) (hf' : ∀ x ∈ f ⁻¹' {y}, ∃ (C : NNReal), AntilipschitzWith C ⇑(f' x)) : (f ⁻¹' {y}).Finite

A compact fibre of regular points is finite. If every point of the fibre of f over y is a point where f has an antilipschitz derivative, for instance an invertible derivative between spaces of the same finite dimension, then each of these points is isolated in the fibre, so a compact fibre is finite.