English
If a C^2 map has an invertible derivative at a point, there exists a neighborhood where nearby derivatives can be written as continuous linear equivalences depending smoothly on the point, with an explicit formula for the derivative of the inverse.
Русский
Если отображение C^2 имеет обратимую производную в точке, то в окрестности существуют непрерывные линейные эквиваленты производных, зависящие плавно от точки, и выражение для производной обратного отображения.
LaTeX
$$$ \\exists N: E \\to (E \\simeq_L[\\mathbb{K}] F),\\; \\text{smoothness conditions and derivative of the inverse exist.}$$$
Lean4
/-- If a `C^2` map has an invertible derivative at a point, then nearby derivatives can be written
as continuous linear equivs, which depend in a `C^1` way on the point, as well as their inverse, and
moreover one can compute the derivative of the inverse. -/
theorem _root_.exists_continuousLinearEquiv_fderiv_symm_eq {f : E → F} {x : E} (h'f : ContDiffAt 𝕜 2 f x)
(hf : (fderiv 𝕜 f x).IsInvertible) :
∃ N : E → (E ≃L[𝕜] F),
ContDiffAt 𝕜 1 (fun y ↦ (N y : E →L[𝕜] F)) x ∧
ContDiffAt 𝕜 1 (fun y ↦ ((N y).symm : F →L[𝕜] E)) x ∧
(∀ᶠ y in 𝓝 x, N y = fderiv 𝕜 f y) ∧
∀ v,
fderiv 𝕜 (fun y ↦ ((N y).symm : F →L[𝕜] E)) x v =
-(N x).symm ∘L ((fderiv 𝕜 (fderiv 𝕜 f) x v)) ∘L (N x).symm :=
by
simp only [← fderivWithin_univ, ← contDiffWithinAt_univ, ← nhdsWithin_univ] at hf h'f ⊢
exact exists_continuousLinearEquiv_fderivWithin_symm_eq h'f hf uniqueDiffOn_univ (mem_univ _)
