English
If a C^2 map has an invertible derivative, there exists a map N such that N and its inverse vary differentiably with x, and N x equals fderiv at x in the appropriate sense, with a formula for the derivative of the inverse.
Русский
Если отображение C^2 имеет обратимую производную, существует N, так что N и его обратное различимо по x, и N x совпадает с fderiv в надлежащем смысле, с формулой производной обратного.
LaTeX
$$$ \\exists N: E \\to (E \\to_L F),\\; \\text{ differentiability properties and inverse derivative formula.}$$$
Lean4
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeo. Variant where unique differentiability and
the invariance property are only required in a smaller set `u`. -/
theorem pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt_of_eventuallyEq {f : E → F} {V W : F → F} {x : E}
{t : Set F} {u : Set E} (hf : IsSymmSndFDerivWithinAt 𝕜 f s x) (h'f : ContDiffWithinAt 𝕜 2 f s x)
(hV : DifferentiableWithinAt 𝕜 V t (f x)) (hW : DifferentiableWithinAt 𝕜 W t (f x)) (hu : UniqueDiffOn 𝕜 u)
(hx : x ∈ u) (hst : MapsTo f u t) (hus : u =ᶠ[𝓝 x] s) :
pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x =
lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x :=
calc
pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) s x
_ = pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W t) u x :=
by
simp only [pullbackWithin]
congr 2
exact fderivWithin_congr_set hus.symm
_ = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V u) (pullbackWithin 𝕜 f W u) u x :=
(pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt (hf.congr_set hus.symm) (h'f.congr_set hus.symm) hV hW
hu hx hst)
_ = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) u x :=
by
apply Filter.EventuallyEq.lieBracketWithin_vectorField_eq_of_mem _ _ hx
· apply nhdsWithin_le_nhds
filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy
simp [pullbackWithin, hy]
· apply nhdsWithin_le_nhds
filter_upwards [fderivWithin_eventually_congr_set (𝕜 := 𝕜) (f := f) hus] with y hy
simp [pullbackWithin, hy]
_ = lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V s) (pullbackWithin 𝕜 f W s) s x := lieBracketWithin_congr_set hus
