The inverse function theorem with a C^n inverse on a whole open set

Mathlib's ContDiffAt.toOpenPartialHomeomorph turns a C^n map with invertible derivative at a point into an OpenPartialHomeomorph, but ContDiffAt.to_localInverse only produces a C^n inverse at the image point: OpenPartialHomeomorph.contDiffAt_symm needs an invertible derivative at the point one inverts around, and invertibility is assumed at the base point alone. Building a partial diffeomorphism of manifolds, or comparing two implicit-function charts of a level set, needs more: the inverse has to be C^n on the whole target.

The invertibility does in fact persist. Mathlib's construction goes through ApproximatesLinearOn: the source of the homeomorphism is an open set on which the map approximates its derivative L at the base point with a constant c strictly below ‖L⁻¹‖⁻¹. On such a set every Fréchet derivative of the map is within c of L in norm, hence is still invertible by ContinuousLinearMap.isInvertible_of_norm_sub_le_half. This file extracts that estimate and runs Mathlib's smooth inverse function theorem at every point of the target.

Two forms are given. The first is about Mathlib's own homeomorphism, over an arbitrary nontrivially normed field: strict differentiability alone makes derivative invertibility persist, while inverse C^n regularity also assumes the corresponding C^n regularity of the map. It is the form a consumer that cannot choose its homeomorphism — such as the implicit-function chart of a level set — needs. The second packages the classical statement over ℝ or ℂ: a C^n map with invertible derivative at a point of an open set s restricts to an OpenPartialHomeomorph inside s whose inverse is C^n on its target.

Main results

• ApproximatesLinearOn.norm_sub_le_of_hasFDerivAt: on a set where f approximates L with constant c, every derivative of f at an interior point is within c of L.
• HasStrictFDerivAt.approximatesLinearOn_toOpenPartialHomeomorph_source: the source of the inverse function theorem's homeomorphism carries the approximation estimate its construction chose.
• HasStrictFDerivAt.isInvertible_of_mem_toOpenPartialHomeomorph_source: hence the derivative of f is invertible at every point of that source, not only at the base point.
• HasStrictFDerivAt.contDiffAt_toOpenPartialHomeomorph_symm and HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm: the local inverse is C^n at every point of the target, and hence on the target.
• TauCeti.ContDiffOn.exists_openPartialHomeomorph: a C^n map (1 ≤ n) on an open set with invertible derivative at a point restricts to an OpenPartialHomeomorph around that point whose inverse is C^n on the whole target.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.
• The Hopf--Rinow roadmap, Layer 1, "The manifold inverse-function theorem".

theorem ApproximatesLinearOn.norm_sub_le_of_hasFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {L A : E →L[𝕜] F} {s : Set E} {c : NNReal} (hf : ApproximatesLinearOn f L s c) {x : E} (hs : s ∈ nhds x) (hA : HasFDerivAt f A x) : ‖A - L‖ ≤ ↑c

On a set on which f approximates the continuous linear map L with constant c, every Fréchet derivative of f at an interior point is within c of L in operator norm.

theorem HasStrictFDerivAt.approximatesLinearOn_toOpenPartialHomeomorph_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {L : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑L) a) : ApproximatesLinearOn f (↑L) (toOpenPartialHomeomorph f hf).source (‖↑L.symm‖₊⁻¹ / 2)

On the source of the homeomorphism built by the inverse function theorem, f approximates its derivative at the base point with the constant ‖L⁻¹‖⁻¹ / 2 that the construction chose.

theorem HasStrictFDerivAt.isInvertible_of_mem_toOpenPartialHomeomorph_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {L : E ≃L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f (↑L) a) {x : E} (hx : x ∈ (toOpenPartialHomeomorph f hf).source) {A : E →L[𝕜] F} (hA : HasFDerivAt f A x) : A.IsInvertible

The derivative of f is invertible throughout the inverse-function neighbourhood. Invertibility of the derivative is assumed at the base point only, but it propagates to every point of the source of HasStrictFDerivAt.toOpenPartialHomeomorph.

theorem HasStrictFDerivAt.contDiffAt_toOpenPartialHomeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {L : E ≃L[𝕜] F} {a : E} {n : WithTop ℕ∞} (hf : HasStrictFDerivAt f (↑L) a) {y : F} (hy : y ∈ (toOpenPartialHomeomorph f hf).target) (hcont : ContDiffAt 𝕜 n f (↑(toOpenPartialHomeomorph f hf).symm y)) : ContDiffAt 𝕜 n (↑(toOpenPartialHomeomorph f hf).symm) y

The local inverse of the inverse function theorem is C^n at every point of its target. The original inverse-function hypotheses provide an invertible derivative only at the base point. Here we prove the missing invertibility throughout the constructed source, then apply Mathlib's OpenPartialHomeomorph.contDiffAt_symm pointwise on the target.

theorem HasStrictFDerivAt.contDiffOn_toOpenPartialHomeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] {f : E → F} {L : E ≃L[𝕜] F} {a : E} {n : WithTop ℕ∞} (hf : HasStrictFDerivAt f (↑L) a) (hcont : ContDiffOn 𝕜 n f (toOpenPartialHomeomorph f hf).source) : ContDiffOn 𝕜 n (↑(toOpenPartialHomeomorph f hf).symm) (toOpenPartialHomeomorph f hf).target

The inverse function theorem produces a C^n inverse. If f is C^n on the source of the homeomorphism built by the inverse function theorem, then the inverse is C^n on the target.

theorem TauCeti.ContDiffOn.exists_openPartialHomeomorph {𝕂 : Type u_1} [RCLike 𝕂] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕂 E] [CompleteSpace E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕂 F] {n : WithTop ℕ∞} {g : E → F} {s : Set E} {a : E} (hg : ContDiffOn 𝕂 n g s) (hs : IsOpen s) (ha : a ∈ s) (hn : 1 ≤ n) {e : E ≃L[𝕂] F} (he : ↑e = fderiv 𝕂 g a) : ∃ (Θ : OpenPartialHomeomorph E F), ↑Θ = g ∧ a ∈ Θ.source ∧ Θ.source ⊆ s ∧ ContDiffOn 𝕂 n (↑Θ.symm) Θ.target

The inverse function theorem, with a C^n inverse on the whole target. A map which is C^n on an open set s, with 1 ≤ n, and whose derivative at a ∈ s is a continuous linear equivalence, coincides on a neighbourhood of a with an OpenPartialHomeomorph whose source is contained in s and whose inverse is C^n on its target.